Fri, 19 Mar 2010 10:24:16 +0100 |
Cezary Kaliszyk |
Remove atom_decl from the parser.
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 23:19:55 +0100 |
Cezary Kaliszyk |
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 15:13:20 +0100 |
Cezary Kaliszyk |
Rename "_property" to ".property"
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 14:05:49 +0100 |
Cezary Kaliszyk |
case names also for _induct
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 12:32:03 +0100 |
Cezary Kaliszyk |
Case_Names for _inducts. Does not work for _induct yet.
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 12:09:59 +0100 |
Cezary Kaliszyk |
Added fv,bn,distinct,perm to the simplifier.
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 08:03:42 +0100 |
Cezary Kaliszyk |
Move most of the exporting out of the parser.
|
file |
diff |
annotate
|