Newsgroup:
fa.isabelle
Add New Display Options
2
replies
[isabelle] Sledgehammer 2015 oddity
started 2015-05-28 05:54:20 UTC
2015-05-30 21:31:04 UTC
Eugene W. Stark
17
replies
[isabelle] Isabelle style guide
started 2015-05-23 10:24:23 UTC
2015-05-30 21:17:37 UTC
Makarius
2
replies
[isabelle] Nitpick falsely produces genuine counterexample
started 2015-05-28 09:00:31 UTC
2015-05-29 15:26:10 UTC
Jasmin Blanchette
2
replies
[isabelle] Eta-expansion of .elims generated by fun
started 2015-05-29 08:09:57 UTC
2015-05-29 10:44:45 UTC
Andreas Lochbihler
14
replies
[isabelle] Moving the AFP away from SourceForge
started 2015-05-28 09:20:01 UTC
2015-05-28 14:57:52 UTC
Till Mossakowski
1
reply
[isabelle] The type class for integer division
started 2015-05-27 16:17:18 UTC
2015-05-28 07:50:29 UTC
Florian Haftmann
9
replies
[isabelle] RC5: Ordering of normal output and error output
started 2015-05-21 12:13:17 UTC
2015-05-27 10:40:37 UTC
Larry Paulson
1
reply
[isabelle] Announcing Isabelle2015
started 2015-05-26 18:34:06 UTC
2015-05-26 22:39:33 UTC
Larry Paulson
1
reply
[isabelle] Context in resolve_tac and rtac
started 2015-05-26 10:38:28 UTC
2015-05-26 10:55:44 UTC
Larry Paulson
2
replies
[isabelle] qualified with fun/inductive/primrec does not qualify generated theorem names.
started 2015-05-22 08:03:27 UTC
2015-05-26 05:00:35 UTC
Lochbihler Andreas
4
replies
[isabelle] Isabelle2015-RC5 available for final testing
started 2015-05-17 23:16:58 UTC
2015-05-23 19:03:48 UTC
Daniel Matichuk
1
reply
[isabelle] Isabelle2015-RC5 ignores document files
started 2015-05-23 13:49:16 UTC
2015-05-23 15:30:31 UTC
Makarius
1
reply
[isabelle] Isabelle2015-RC5 - minor feature request
started 2015-05-23 13:20:09 UTC
2015-05-23 13:48:09 UTC
Makarius
4
replies
[isabelle] RC5: Many Grayouts if many theory files are loaded
started 2015-05-21 09:41:31 UTC
2015-05-21 12:43:16 UTC
Makarius
2
replies
[isabelle] RC5: Running sledgehammer still blocks output
started 2015-05-19 16:23:34 UTC
2015-05-20 07:59:06 UTC
Peter Lammich
22
replies
[isabelle] libisabelle: Small Scala library to communicate with Isabelle
started 2015-02-09 14:19:01 UTC
2015-05-19 08:21:04 UTC
Walther Neuper
2
replies
[isabelle] Equivalent to schematic_lemma inside proof blocks
started 2015-05-18 10:53:51 UTC
2015-05-18 13:43:21 UTC
Andreas Lochbihler
1
reply
[isabelle] polyml 64bit Darwin heap size
started 2015-05-16 23:07:53 UTC
2015-05-16 23:16:13 UTC
Gerwin Klein
9
replies
[isabelle] Polymorphic predicate closed under composition
started 2015-05-13 15:45:26 UTC
2015-05-15 18:55:17 UTC
Andreas Lochbihler
9
replies
[isabelle] Document preparation hints
started 2014-01-07 15:24:09 UTC
2015-05-15 13:31:35 UTC
Mathias Fleury
5
replies
[isabelle] Bets Practice for local helper lemmas
started 2015-05-04 20:01:42 UTC
2015-05-13 18:55:43 UTC
Makarius
9
replies
[isabelle] simp warnings for cong rules
started 2015-05-11 08:32:53 UTC
2015-05-13 15:17:26 UTC
Makarius
1
reply
[isabelle] Extracting Goal Information from Proof Terms
started 2015-05-12 10:13:03 UTC
2015-05-13 07:25:47 UTC
Mandy Martin
3
replies
[isabelle] Probabilities: expectation as a sum
started 2015-05-05 15:36:55 UTC
2015-05-12 09:25:21 UTC
Johannes Hölzl
3
replies
[isabelle] Cyclic graphs
started 2015-05-06 15:35:51 UTC
2015-05-11 19:07:13 UTC
Florian Haftmann
6
replies
[isabelle] Let and commutative rewrite rules
started 2015-05-04 14:02:24 UTC
2015-05-11 19:05:40 UTC
Florian Haftmann
7
replies
[isabelle] Perl Module Missing (Isabelle-RC3 on Linux)
started 2015-05-11 00:10:43 UTC
2015-05-11 15:58:31 UTC
Alfio Martini
1
reply
[isabelle] Qualified/Private with lifting package in Isabelle2015-RC4
started 2015-05-11 07:01:06 UTC
2015-05-11 12:59:54 UTC
Ondřej Kunčar
24
replies
[isabelle] Isabelle2015-RC3 available for testing
started 2015-05-04 21:47:43 UTC
2015-05-08 15:34:58 UTC
Makarius
4
replies
[isabelle] Sledgehammer on Windows
started 2015-05-07 20:18:35 UTC
2015-05-08 14:01:09 UTC
Alfio Martini
Click to Load More...
Loading...