Newsgroup:
fa.isabelle
Add newDisplay options
3
replies
[isabelle] Don’t Make Your Readers Scream
started 2014-12-16 14:37:39 UTC
2014-12-18 23:28:59 UTC
Lawrence Paulson
1
reply
[isabelle] Theorem dependencies in jEdit
started 2014-12-18 10:58:32 UTC
2014-12-18 13:11:48 UTC
Makarius
1
reply
[isabelle] Scala codegen error: need NatO, natT, and NatC
started 2014-12-18 01:08:13 UTC
2014-12-18 05:45:19 UTC
Gottfried Barrow
1
reply
[isabelle] export_code ... checking
started 2014-12-09 15:09:24 UTC
2014-12-17 08:24:36 UTC
Florian Haftmann
5
replies
[isabelle] Experimental tweaks to make HOL intuitionistic-by-default
started 2014-11-21 22:12:07 UTC
2014-12-15 21:23:46 UTC
Josh Tilles
1
reply
[isabelle] Prover Process terminated!?
started 2014-12-12 16:05:52 UTC
2014-12-15 19:21:21 UTC
Makarius
13
replies
[isabelle] resolve current subgoal with matching premise
started 2014-12-04 21:16:23 UTC
2014-12-15 17:10:25 UTC
Makarius
1
reply
[isabelle] Parallelising apply-style proofs
started 2014-12-11 22:02:37 UTC
2014-12-13 09:41:59 UTC
Makarius
2
replies
[isabelle] TERM exception in fologic.ML
started 2014-10-27 19:40:19 UTC
2014-12-12 03:15:48 UTC
Thomas Sewell
2
replies
[isabelle] Discharging non-atomic assumptions in Isabelle/ML
started 2014-12-09 09:42:03 UTC
2014-12-10 10:13:46 UTC
Makarius
1
reply
[isabelle] isar-ref: railsetup
started 2014-12-09 13:12:30 UTC
2014-12-09 13:57:36 UTC
Makarius
1
reply
[isabelle] antiquotation @{command ...}
started 2014-12-09 11:24:25 UTC
2014-12-09 13:55:37 UTC
Makarius
3
replies
[isabelle] running bibtex through document preparation
started 2014-12-08 12:07:12 UTC
2014-12-08 18:30:15 UTC
Makarius
4
replies
[isabelle] named theorems in Isabelle/ML
started 2014-12-05 21:21:56 UTC
2014-12-08 16:49:56 UTC
Christian Sternagel
1
reply
[isabelle] rule is sometimes very slow
started 2014-12-02 15:26:37 UTC
2014-12-08 16:26:55 UTC
Makarius
4
replies
[isabelle] simp_trace_new
started 2014-12-04 16:28:44 UTC
2014-12-08 15:55:47 UTC
Makarius
26
replies
[isabelle] Isabelle2014-RC2: PIDE does not resume processing
started 2014-08-08 12:55:50 UTC
2014-12-08 10:08:56 UTC
Makarius
1
reply
[isabelle] Argument types problem
started 2014-12-03 20:11:52 UTC
2014-12-03 20:57:10 UTC
Makarius
7
replies
[isabelle] Hoare-Logic-bubble_Sort
started 2014-11-28 09:45:36 UTC
2014-12-01 21:36:05 UTC
Gerwin Klein
1
reply
[isabelle] thin_tac
started 2014-11-27 17:04:22 UTC
2014-12-01 15:43:21 UTC
Makarius
1
reply
[isabelle] Fact completion
started 2014-11-27 16:42:26 UTC
2014-11-27 17:19:21 UTC
Peter Lammich
1
reply
[isabelle] Ambiguous input
started 2014-11-27 14:52:10 UTC
2014-11-27 15:03:59 UTC
René Thiemann
5
replies
[isabelle] emergence of "TERM _" (using quickcheck and nitpick)
started 2014-11-20 18:30:26 UTC
2014-11-27 12:14:48 UTC
Daniel Raggi
1
reply
[isabelle] Cl-isabelle-users Digest, Vol 113, Issue 26
started 2014-11-25 15:43:52 UTC
2014-11-26 11:07:55 UTC
Florian Haftmann
1
reply
[isabelle] Array
started 2014-11-25 14:52:39 UTC
2014-11-25 15:27:23 UTC
Peter Lammich
2
replies
[isabelle] Define a fun
started 2014-11-25 13:05:02 UTC
2014-11-25 13:26:10 UTC
Peter Lammich
1
reply
[isabelle] Isar-Level cases command
started 2014-11-25 10:00:49 UTC
2014-11-25 10:45:14 UTC
Andreas Lochbihler
13
replies
[isabelle] Disproof methods with Word.thy and AutoCorres
started 2014-11-04 17:45:42 UTC
2014-11-24 16:57:05 UTC
Jasmin Christian Blanchette
14
replies
[isabelle] replace "isabelle tty"
started 2014-11-18 15:54:53 UTC
2014-11-24 16:00:01 UTC
Makarius
2
replies
[isabelle] TYPE_MATCH exception with adhoc_overloading
started 2014-11-21 18:34:54 UTC
2014-11-23 10:50:46 UTC
Dmitriy Traytel
Click to Load More...