Newsgroup:
fa.isabelle
Add New Display Options
4
replies
[isabelle] Well-foundedness of Relational Composition
started 2015-04-24 14:39:02 UTC
2015-04-27 11:48:33 UTC
Tjark Weber
1
reply
[isabelle] How to "code abstract" over nested types
started 2015-04-26 12:57:09 UTC
2015-04-27 06:46:32 UTC
Andreas Lochbihler
1
reply
[isabelle] Division-ring for fields
started 2015-04-24 13:13:36 UTC
2015-04-26 15:26:56 UTC
Florian Haftmann
2
replies
[isabelle] RC-1 – ad 8bd5999133d4 – »code_deps needs cycles«
started 2015-04-21 19:29:02 UTC
2015-04-26 15:23:06 UTC
Florian Haftmann
4
replies
[isabelle] What is sumC?
started 2015-04-24 19:29:59 UTC
2015-04-26 07:20:19 UTC
Lars Hupel
9
replies
[isabelle] Difficulties with "setsum" (Alfio Martini)
started 2015-04-23 00:36:23 UTC
2015-04-25 22:50:27 UTC
Alfio Martini
39
replies
[isabelle] Isabelle2015-RC0 available for testing
started 2015-04-11 19:57:18 UTC
2015-04-24 22:28:57 UTC
Makarius
4
replies
[isabelle] Isabelle2015-RC1 available for testing
started 2015-04-17 20:36:03 UTC
2015-04-24 22:23:47 UTC
Makarius
18
replies
[isabelle] libisabelle: Small Scala library to communicate with Isabelle
started 2015-02-09 14:19:01 UTC
2015-04-24 15:24:02 UTC
Lars Hupel
1
reply
[isabelle] Program extraction, accessing instantiated proof terms
started 2015-04-20 15:47:07 UTC
2015-04-24 14:17:58 UTC
Stefan Berghofer
4
replies
[isabelle] Isabelle2015-RC1: Rule instantiation in Eisbach
started 2015-04-20 12:56:06 UTC
2015-04-24 11:13:11 UTC
Daniel Matichuk
5
replies
[isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal
started 2015-04-23 09:52:25 UTC
2015-04-24 09:32:30 UTC
Larry Paulson
5
replies
[isabelle] Difficulties with "setsum"
started 2015-04-22 15:02:30 UTC
2015-04-22 19:21:07 UTC
Lars Hupel
6
replies
[isabelle] print_cases shows non-existing schematic variable
started 2015-04-22 08:48:37 UTC
2015-04-22 14:15:58 UTC
Lars Hupel
2
replies
[isabelle] Illegal schematic variable(s) in case
started 2015-04-20 13:03:39 UTC
2015-04-22 08:50:14 UTC
Lars Hupel
4
replies
[isabelle] primcorec does not terminate
started 2015-04-16 19:27:19 UTC
2015-04-21 06:35:17 UTC
Jasmin Blanchette
4
replies
[isabelle] add_assoc, add.assoc and reflection
started 2015-04-20 06:44:52 UTC
2015-04-20 11:47:23 UTC
Walther Neuper
1
reply
[isabelle] Syntax diagram for obtains allows "is" bindings
started 2015-04-09 10:12:24 UTC
2015-04-18 19:05:12 UTC
Makarius
3
replies
[isabelle] HOL-Word contains trivial lemmas
started 2015-04-16 15:42:17 UTC
2015-04-18 09:36:11 UTC
Florian Haftmann
2
replies
[isabelle] "Stuck" (i.e. looping) prover issues
started 2015-04-14 21:28:36 UTC
2015-04-17 22:52:19 UTC
Makarius
6
replies
[isabelle] Isabelle: A logic of total functions (?)
started 2015-04-17 13:58:31 UTC
2015-04-17 16:52:42 UTC
Larry Paulson
6
replies
[isabelle] \forall versus \And -- also \exists versus \Or
started 2015-04-07 02:33:46 UTC
2015-04-16 22:17:33 UTC
Makarius
1
reply
[isabelle] Strange simplifier behaviour
started 2015-04-01 15:02:32 UTC
2015-04-16 22:03:36 UTC
Makarius
4
replies
[isabelle] ind_cases appears to ignore chained facts
started 2015-03-18 10:31:42 UTC
2015-04-16 20:43:05 UTC
Makarius
3
replies
[isabelle] Problem with Int.int_ge_induct
started 2015-04-14 04:46:34 UTC
2015-04-16 07:36:19 UTC
Lars Noschinski
1
reply
[isabelle] error encountered while parsing in autocorres
started 2015-04-15 09:58:13 UTC
2015-04-15 14:32:51 UTC
Gerwin Klein
4
replies
[isabelle] Tuning opportunity for auto-completion in Isabelle/Jedit
started 2015-04-13 14:20:11 UTC
2015-04-15 09:19:06 UTC
Bertram Felgenhauer
3
replies
[isabelle] interpretation and sublocale add Pure.prop to ?thesis
started 2015-04-01 09:24:04 UTC
2015-04-14 19:20:49 UTC
Makarius
5
replies
[isabelle] Unknown Isabelle tool: env
started 2015-04-11 13:00:58 UTC
2015-04-14 14:18:08 UTC
Makarius
1
reply
[isabelle] Isabelle2015-RC0 ML ATP_Util.unyxml
started 2015-04-13 13:27:24 UTC
2015-04-14 10:42:52 UTC
Makarius
Click to Load More...
Loading...