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
|
Fri, 31 Dec 2010 15:37:04 +0000 |
Christian Urban |
changed res keyword to set+ for restrictions; comment by a referee
|
file |
diff |
annotate
|
Wed, 22 Dec 2010 21:13:44 +0000 |
Christian Urban |
tuned examples
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 10:28:08 +0000 |
Christian Urban |
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
|
file |
diff |
annotate
|
Sat, 13 Nov 2010 22:23:26 +0000 |
Christian Urban |
lifted permute_bn constants
|
file |
diff |
annotate
|
Fri, 12 Nov 2010 01:20:53 +0000 |
Christian Urban |
automated permute_bn functions (raw ones first)
|
file |
diff |
annotate
|
Wed, 10 Nov 2010 13:46:21 +0000 |
Christian Urban |
adapted to changes by Florian on the quotient package and removed local fix for function package
|
file |
diff |
annotate
|
Thu, 14 Oct 2010 04:14:22 +0100 |
Christian Urban |
major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
|
file |
diff |
annotate
|
Tue, 05 Oct 2010 07:30:37 +0100 |
Christian Urban |
llncs and more sqeezing
|
file |
diff |
annotate
|
Mon, 27 Sep 2010 12:19:17 -0400 |
Christian Urban |
added postprocessed fresh-lemmas for constructors
|
file |
diff |
annotate
|
Mon, 27 Sep 2010 09:51:15 -0400 |
Christian Urban |
post-processed eq_iff and supp threormes according to the fv-supp equality
|
file |
diff |
annotate
|
Mon, 27 Sep 2010 04:56:28 -0400 |
Christian Urban |
some experiments
|
file |
diff |
annotate
|
Sat, 25 Sep 2010 08:38:04 -0400 |
Christian Urban |
lifted size_thms and exported them as <name>.size
|
file |
diff |
annotate
|
Sat, 25 Sep 2010 08:28:45 -0400 |
Christian Urban |
cleaned up two examples
|
file |
diff |
annotate
|
Sat, 18 Sep 2010 06:09:43 +0800 |
Christian Urban |
updated to Isabelle Sept 16
|
file |
diff |
annotate
|