Newsgroup:
fa.isabelle
Add New Display Options
9
replies
[isabelle] [Noob] Proof on trees
started 2016-05-26 17:11:13 UTC
2016-05-29 01:18:31 UTC
Alfio Martini
2
replies
[isabelle] Malformed dependency error with overloading
started 2016-05-27 11:20:58 UTC
2016-05-27 12:10:02 UTC
Andreas Lochbihler
1
reply
[isabelle] Adding lemmas to HOL?
started 2016-05-27 10:13:54 UTC
2016-05-27 11:58:55 UTC
Andreas Lochbihler
3
replies
[isabelle] How to process chained facts in Eisbach method?
started 2016-05-22 10:40:59 UTC
2016-05-27 00:26:09 UTC
Daniel Matichuk
2
replies
[isabelle] Problem with "additional type variables" in a definition
started 2016-05-24 09:35:25 UTC
2016-05-24 15:09:24 UTC
Lars-Henrik Eriksson
2
replies
[isabelle] Isabelle 2005 request
started 2016-05-23 11:07:58 UTC
2016-05-24 12:12:35 UTC
Makarius
1
reply
[isabelle] Isabelle/HOL 2005
started 2016-05-17 19:17:21 UTC
2016-05-24 10:01:40 UTC
Makarius
2
replies
[isabelle] sledgehammer+vampire 4.0 often fails
started 2016-05-23 15:00:11 UTC
2016-05-23 16:24:50 UTC
Christoph Dittmann
2
replies
[isabelle] A single way to reference AFP entries
started 2016-05-20 11:04:55 UTC
2016-05-20 11:56:12 UTC
Lars Hupel
2
replies
[isabelle] Removing trivial premises
started 2016-05-19 19:28:04 UTC
2016-05-20 09:52:23 UTC
Makarius
1
reply
[isabelle] Shortest way to prove an object-level implication via ML
started 2016-05-19 12:50:54 UTC
2016-05-20 09:35:02 UTC
Makarius
1
reply
[isabelle] smt method avoidance
started 2016-05-19 20:19:50 UTC
2016-05-19 20:27:39 UTC
Jasmin Blanchette
5
replies
[isabelle] Lifting package and state transformers
started 2016-05-17 05:01:43 UTC
2016-05-17 18:46:28 UTC
Andreas Lochbihler
3
replies
[isabelle] Inclusion-minimal sets
started 2016-05-14 11:27:44 UTC
2016-05-17 08:21:07 UTC
Manuel Eberl
1
reply
[isabelle] AFP: Theory dependency graphs are empty
started 2016-05-13 14:27:08 UTC
2016-05-13 16:53:51 UTC
Makarius
4
replies
[isabelle] primrec or fun
started 2016-05-11 10:53:39 UTC
2016-05-11 19:23:45 UTC
Jasmin Blanchette
2
replies
[isabelle] unexpected conversion from real to int
started 2016-05-06 14:39:58 UTC
2016-05-09 19:21:16 UTC
Colin Rowat
1
reply
[isabelle] Isabelle2016-RC2: bogus simplifier trace messages
started 2016-01-29 16:14:38 UTC
2016-05-09 16:36:52 UTC
Makarius
4
replies
[isabelle] Isabelle's environment and external executables
started 2016-05-09 11:57:13 UTC
2016-05-09 13:21:18 UTC
Makarius
1
reply
[isabelle] Using typedef_overloaded in future releases of Isabelle
started 2016-05-03 15:36:59 UTC
2016-05-03 23:26:59 UTC
Gerwin Klein
9
replies
[isabelle] unused_thms in proofs
started 2016-04-29 08:44:49 UTC
2016-05-03 14:44:41 UTC
Makarius
1
reply
[isabelle] Current CSP formalisation with syntax and semantics
started 2016-05-03 09:00:58 UTC
2016-05-03 09:44:07 UTC
Makarius
1
reply
[isabelle] Unit-Tests for Isabelle Theories
started 2016-04-27 12:38:23 UTC
2016-04-28 03:15:19 UTC
Thomas Sewell
1
reply
[isabelle] Isabelle2016: sledgehammer ignores prover list
started 2016-04-27 15:18:03 UTC
2016-04-27 19:54:22 UTC
Jasmin Blanchette
1
reply
[isabelle] ML goes "incommunicado" for minutes at a time during sledgehammering
started 2016-04-22 16:10:04 UTC
2016-04-27 07:49:01 UTC
Mathias Fleury
2
replies
[isabelle] New entry in the (moved!) AFP
started 2016-04-26 13:21:58 UTC
2016-04-26 21:59:31 UTC
Gerwin Klein
1
reply
[isabelle] Going from Isabelle 2013 to Isabelle 2016
started 2016-04-25 14:14:58 UTC
2016-04-25 15:21:19 UTC
Makarius
1
reply
[isabelle] Type variables, locale import and notation
started 2016-04-23 23:58:26 UTC
2016-04-25 06:39:23 UTC
Andreas Lochbihler
1
reply
[isabelle] Problem during goal simplification
started 2016-04-21 19:46:11 UTC
2016-04-21 23:13:00 UTC
Omar Montaño Rivas
1
reply
[isabelle] ZF theory - loading problem
started 2016-04-18 13:36:58 UTC
2016-04-18 13:44:57 UTC
Lawrence Paulson
Click to Load More...
Loading...