| Sat, 17 Mar 2012 05:13:59 +0000 |
Christian Urban |
updated to new Isabelle (declared keywords)
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 13:19:23 +0000 |
Christian Urban |
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 18:42:34 +0200 |
Christian Urban |
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
|
file |
diff |
annotate
|
| Tue, 03 May 2011 15:39:30 +0100 |
Christian Urban |
added two mutual recursive inductive definitions
|
file |
diff |
annotate
|
| Wed, 22 Dec 2010 09:13:25 +0000 |
Christian Urban |
properly exported strong exhaust theorem; cleaned up some examples
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 13:36:03 +0800 |
Christian Urban |
renamed NewParser to Nominal2
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 03:37:17 +0800 |
Christian Urban |
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 02:08:00 +0800 |
Christian Urban |
cleaned up (almost completely) the examples
|
file |
diff |
annotate
|
| Mon, 07 Jun 2010 11:43:01 +0200 |
Christian Urban |
work on transitivity proof
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:59:53 +0100 |
Christian Urban |
fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
|
file |
diff |
annotate
|
| Tue, 11 May 2010 18:20:25 +0200 |
Cezary Kaliszyk |
Include raw permutation definitions in eqvt
|
file |
diff |
annotate
|
| Tue, 11 May 2010 17:16:57 +0200 |
Cezary Kaliszyk |
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
|
file |
diff |
annotate
|
| Mon, 10 May 2010 17:55:54 +0100 |
Christian Urban |
fixing bind_set problem
|
file |
diff |
annotate
|
| Sun, 09 May 2010 12:38:59 +0100 |
Christian Urban |
tuned file names for examples
|
file |
diff |
annotate
| base
|