Newsgroup:
fa.isabelle
Add New Display Options
6
replies
[isabelle] Parametrized transfer rules with lift_definition
started 2016-06-10 15:36:45 UTC
2016-06-24 14:27:35 UTC
Andreas Lochbihler
2
replies
[isabelle] AFP submission site is unavailable?
started 2016-06-23 20:14:23 UTC
2016-06-23 21:17:45 UTC
Lars Hupel
3
replies
[isabelle] Permutations
started 2016-06-23 08:07:15 UTC
2016-06-23 10:07:31 UTC
Christian Sternagel
1
reply
[isabelle] Specification.definition: Getting theorem for Const, not Free?
started 2016-06-22 23:36:55 UTC
2016-06-23 06:31:05 UTC
Lars Hupel
2
replies
[isabelle] Parametricity for functions which ignore arguments
started 2016-06-20 07:44:47 UTC
2016-06-22 17:11:04 UTC
Andrei Popescu
3
replies
[isabelle] Malformed dependency error with overloading
started 2016-05-27 11:20:58 UTC
2016-06-20 15:28:06 UTC
Simon Foster
1
reply
[isabelle] Question about code generation
started 2016-06-15 06:43:13 UTC
2016-06-16 18:44:38 UTC
Jørgen Villadsen
3
replies
[isabelle] lift_definition in locales
started 2016-06-15 18:51:36 UTC
2016-06-16 12:22:26 UTC
Mathias Fleury
1
reply
[isabelle] Operator clash for $
started 2016-06-16 09:57:07 UTC
2016-06-16 10:13:39 UTC
Andreas Lochbihler
2
replies
[isabelle] Operator with Pair sets
started 2016-06-16 08:45:02 UTC
2016-06-16 09:32:59 UTC
Andreas Lochbihler
2
replies
[isabelle] Opaque ascription for SML code generation
started 2016-06-10 18:28:52 UTC
2016-06-14 17:01:32 UTC
Jørgen Villadsen
2
replies
[isabelle] Large theories
started 2016-06-07 11:31:45 UTC
2016-06-09 09:03:35 UTC
Станислав Владимирович Моисеев
3
replies
[isabelle] Fwd: Executing 2 Isabelle-2016 or even 2 Jedit processes on Windows
started 2016-06-08 09:09:56 UTC
2016-06-08 21:53:26 UTC
Nemouchi Yakoub
3
replies
[isabelle] Turnstile
started 2016-06-06 23:57:25 UTC
2016-06-07 13:12:38 UTC
Makarius
5
replies
[isabelle] Set Comprehention {5n. n€N} without existence-quantor?
started 2016-06-06 11:10:12 UTC
2016-06-06 11:35:25 UTC
Jonathan Woodgate via Cl-isabelle-users
12
replies
[isabelle] Algebraic_Numbers
started 2016-06-02 07:36:25 UTC
2016-06-04 12:19:28 UTC
Makarius
5
replies
[isabelle] SAT solver problem
started 2016-06-02 09:43:07 UTC
2016-06-02 19:11:56 UTC
Makarius
1
reply
[isabelle] Printing natural numbers
started 2016-05-31 07:10:46 UTC
2016-06-02 07:33:55 UTC
Manuel Eberl
2
replies
[isabelle] theoretical question
started 2016-05-31 09:43:54 UTC
2016-06-01 10:33:14 UTC
Lawrence Paulson
2
replies
[isabelle] Questions about Quickcheck
started 2016-05-30 11:29:53 UTC
2016-06-01 06:20:26 UTC
Lukas Bulwahn
3
replies
[isabelle] Problem with "additional type variables" in a definition
started 2016-05-24 09:35:25 UTC
2016-05-30 18:54:16 UTC
Makarius
3
replies
[isabelle] A single way to reference AFP entries
started 2016-05-20 11:04:55 UTC
2016-05-30 18:12:04 UTC
Makarius
3
replies
[isabelle] Isabelle 2005 request
started 2016-05-23 11:07:58 UTC
2016-05-30 12:49:32 UTC
Rajeev Gore
9
replies
[isabelle] [Noob] Proof on trees
started 2016-05-26 17:11:13 UTC
2016-05-29 01:18:31 UTC
Alfio Martini
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
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] 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
Click to Load More...
Loading...