Newsgroup:
fa.isabelle
9
replies
[isabelle] case_names
started 2015-03-26 01:42:20 UTC
2015-03-28 13:39:49 UTC
marco caminati
1
reply
[isabelle] Semirings in HOL/Algebra/Ring
started 2015-03-27 14:21:31 UTC
2015-03-27 14:31:09 UTC
Larry Paulson
1
reply
[isabelle] More strange locale behavior
started 2015-03-24 21:54:14 UTC
2015-03-26 09:42:27 UTC
Florian Haftmann
3
replies
[isabelle] Differences between code_reflect and export_code
started 2015-03-24 16:01:53 UTC
2015-03-26 09:42:14 UTC
Lars Hupel
1
reply
[isabelle] Proposal for code generator: Warning when functions get additional class constraints
started 2015-03-20 08:18:42 UTC
2015-03-26 09:35:00 UTC
Florian Haftmann
2
replies
[isabelle] _graph _grap_aux and _sumC
started 2015-03-25 14:18:29 UTC
2015-03-25 15:33:40 UTC
Christian Sternagel
2
replies
[isabelle] ind_cases appears to ignore chained facts
started 2015-03-18 10:31:42 UTC
2015-03-25 14:20:37 UTC
Makarius
4
replies
[isabelle] Induction starting from 1 and beyond
started 2015-03-24 19:43:28 UTC
2015-03-25 12:55:28 UTC
Christian Sternagel
2
replies
[isabelle] simplifier tracing
started 2015-03-18 14:33:36 UTC
2015-03-22 10:53:20 UTC
Lars Hupel
1
reply
[isabelle] flat function exists in Isabelle lib?
started 2015-03-22 01:03:32 UTC
2015-03-22 01:37:01 UTC
Gerwin Klein
7
replies
[isabelle] Are the countable sets a ccpo
started 2015-03-20 15:14:21 UTC
2015-03-21 13:16:20 UTC
Lochbihler Andreas
1
reply
[isabelle] Abruptly Terminating a State Monad
started 2015-03-18 16:44:14 UTC
2015-03-21 01:57:54 UTC
Gerwin Klein
6
replies
[isabelle] Rewriting nat numerals to Suc notation
started 2015-03-18 15:17:22 UTC
2015-03-20 12:44:52 UTC
Makarius
12
replies
[isabelle] Rearranging equations before taking limits
started 2015-03-04 20:16:13 UTC
2015-03-19 23:01:22 UTC
Aadish Kumar
3
replies
[isabelle] Quotient Type Definition: Map and Relator
started 2015-03-19 13:43:35 UTC
2015-03-19 17:04:00 UTC
Ondřej Kunčar
1
reply
[isabelle] Strange errors involving locales
started 2015-03-19 10:20:26 UTC
2015-03-19 11:23:33 UTC
Andreas Lochbihler
4
replies
[isabelle] Introducing a BNF for Sets of Bounded Cardinality
started 2015-03-14 00:25:30 UTC
2015-03-19 07:56:57 UTC
Dmitriy Traytel
1
reply
[isabelle] f(m+int(z+1)) = f(m+int(z)+1)
started 2015-03-18 22:44:09 UTC
2015-03-19 06:31:58 UTC
Thiemann, Rene
1
reply
[isabelle] Antiquotations
started 2015-03-17 21:15:29 UTC
2015-03-18 07:51:28 UTC
Lars Noschinski
2
replies
[isabelle] well-founded induction on the length of a list
started 2015-03-15 17:46:26 UTC
2015-03-17 19:04:57 UTC
Amarin Phaosawasdi
2
replies
[isabelle] Work on a new theorem prover
started 2015-03-17 09:59:11 UTC
2015-03-17 18:56:40 UTC
Bohua Zhan
7
replies
[isabelle] Storing Generic_Data in a local theory
started 2015-03-08 11:18:03 UTC
2015-03-16 15:23:52 UTC
Makarius
1
reply
[isabelle] Reddit over, or in conjunction, with Stackoverflow?
started 2015-03-15 13:30:12 UTC
2015-03-16 15:05:27 UTC
Makarius
2
replies
[isabelle] OFCLASS and locale.class
started 2015-03-13 19:48:56 UTC
2015-03-14 19:10:36 UTC
Thiemann, Rene
9
replies
[isabelle] Weakest precondition of WHILE as a least fixed point
started 2015-03-11 15:41:17 UTC
2015-03-12 16:29:39 UTC
David Cock
4
replies
[isabelle] linarith for enat
started 2015-03-06 14:39:03 UTC
2015-03-10 15:39:34 UTC
Andreas Lochbihler
3
replies
[isabelle] Reasoning about static variables in AutoCorres
started 2015-03-03 17:33:56 UTC
2015-03-09 22:07:07 UTC
Gerwin Klein
11
replies
[isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?
started 2015-03-03 12:31:15 UTC
2015-03-09 20:34:02 UTC
Makarius
3
replies
[isabelle] Jedit and export_code
started 2015-03-06 19:50:28 UTC
2015-03-06 20:14:30 UTC
Makarius
1
reply
[isabelle] Associativity of conj not picked up by blast
started 2015-03-06 15:31:20 UTC
2015-03-06 17:46:03 UTC
Makarius
Click to Load More...
Loading...