Newsgroup:
fa.isabelle
Add New Display Options
1
reply
[isabelle] lset contains unexpected elements
started 2015-08-04 16:03:38 UTC
2015-08-04 16:13:45 UTC
Jasmin Blanchette
1
reply
[isabelle] Parametrisation of transfer rules
started 2015-08-04 10:13:17 UTC
2015-08-04 16:05:42 UTC
Ondřej Kunčar
1
reply
[isabelle] document generation for selected theories only
started 2015-07-30 12:12:52 UTC
2015-08-04 09:17:34 UTC
Makarius
1
reply
[isabelle] Some useful lemmas for multisets.
started 2015-08-03 07:07:34 UTC
2015-08-04 04:35:53 UTC
Thomas Sewell
4
replies
[isabelle] Sledgehammer 2015 oddity
started 2015-05-28 05:54:20 UTC
2015-08-02 16:44:56 UTC
Eugene W. Stark
3
replies
[isabelle] Ubuntu - All external provers suddenly segfaulting
started 2015-07-29 07:54:56 UTC
2015-07-30 14:01:00 UTC
C. Diekmann
2
replies
[isabelle] Precedences of map_upd vs. fun_upd
started 2015-07-29 15:01:56 UTC
2015-07-30 10:32:54 UTC
Andreas Lochbihler
2
replies
[isabelle] Implementing the higher-order logic Q0 within the Isabelle proof assistant software
started 2015-07-28 09:24:02 UTC
2015-07-30 09:28:20 UTC
Ken Kubota
7
replies
[isabelle] Creating ML data is slow. No sharing/caching?
started 2015-07-28 18:22:45 UTC
2015-07-29 22:20:49 UTC
Gerwin Klein
2
replies
[isabelle] using HOL.contrapos_pp
started 2015-07-28 18:49:40 UTC
2015-07-28 20:52:49 UTC
Makarius
3
replies
[isabelle] Contracting Abbreviations of Locale Definitions
started 2015-07-27 19:21:39 UTC
2015-07-28 10:16:00 UTC
Andreas Lochbihler
3
replies
[isabelle] apply x apply y vs. by x y
started 2015-07-27 20:38:25 UTC
2015-07-28 07:42:39 UTC
Lars Noschinski
6
replies
[isabelle] Quotients and code generation for higher-order functions
started 2015-07-24 06:58:35 UTC
2015-07-27 07:10:39 UTC
Andreas Lochbihler
2
replies
[isabelle] AFP repository now on bitbucket
started 2015-07-26 11:12:50 UTC
2015-07-26 23:22:33 UTC
Gerwin Klein
4
replies
[isabelle] Record selectors operate only on _scheme and not on _ext?
started 2015-07-20 07:41:19 UTC
2015-07-22 16:48:45 UTC
Andreas Lochbihler
4
replies
[isabelle] @{context}
started 2015-07-20 11:09:15 UTC
2015-07-21 18:48:31 UTC
Buday Gergely
2
replies
[isabelle] Parametricity for records
started 2015-07-20 07:29:33 UTC
2015-07-21 07:56:57 UTC
Andreas Lochbihler
3
replies
[isabelle] Problems with transfer_prover
started 2015-07-17 15:10:43 UTC
2015-07-20 09:17:41 UTC
Mandy Martin
8
replies
[isabelle] writing an Isar proof for multiple subgoals
started 2015-07-13 12:08:49 UTC
2015-07-17 12:12:15 UTC
Lars Noschinski
1
reply
[isabelle] Short syntax for "solves <method>"
started 2015-07-16 11:30:13 UTC
2015-07-16 13:30:58 UTC
Andreas Lochbihler
2
replies
[isabelle] exception UnequalLengths raised (line 543 of "library.ML")
started 2015-07-15 06:19:55 UTC
2015-07-15 17:38:31 UTC
Jason Dagit
1
reply
[isabelle] using identity for simplification with different type
started 2015-07-15 16:48:11 UTC
2015-07-15 17:15:04 UTC
Lars Noschinski
1
reply
[isabelle] inductive_set with non-fixed parameters
started 2015-07-15 11:08:57 UTC
2015-07-15 13:17:40 UTC
Andreas Lochbihler
1
reply
[isabelle] Destruction rules setup
started 2015-07-14 20:59:45 UTC
2015-07-15 05:15:49 UTC
Lars Noschinski
2
replies
[isabelle] Auto has to be invoked twice to succeed
started 2015-07-14 15:49:38 UTC
2015-07-14 15:58:37 UTC
Lars Noschinski
1
reply
[isabelle] Reflexive rewriting
started 2015-07-13 12:11:25 UTC
2015-07-13 12:27:11 UTC
Makarius
2
replies
[isabelle] Destruction rule setup
started 2015-07-12 11:21:51 UTC
2015-07-13 12:08:43 UTC
Makarius
7
replies
[isabelle] Incompleteness and Nominal2
started 2015-07-07 15:46:05 UTC
2015-07-09 11:23:04 UTC
Christian Urban
6
replies
[isabelle] libisabelle: embedding on Java-side
started 2015-07-04 07:24:02 UTC
2015-07-09 10:28:43 UTC
Walther Neuper
1
reply
[isabelle] Quickcheck setup for finite sets
started 2015-07-08 10:27:01 UTC
2015-07-08 14:06:47 UTC
Lars Hupel
Click to Load More...
Loading...