| Fri, 19 Mar 2010 18:42:57 +0100 |
Cezary Kaliszyk |
Automatically derive support for datatypes with at-most one binding per constructor.
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 14:54:30 +0100 |
Cezary Kaliszyk |
Use fs typeclass in showing finite support + some cheat cleaning.
|
file |
diff |
annotate
|
| 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
|
| Thu, 18 Mar 2010 07:43:44 +0100 |
Cezary Kaliszyk |
Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 07:35:44 +0100 |
Cezary Kaliszyk |
Prove eqvts on exported terms.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 07:26:36 +0100 |
Cezary Kaliszyk |
Clean 'Lift', start working only on exported things in Parser.
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 17:11:23 +0100 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 15:13:31 +0100 |
Christian Urban |
made paper to compile
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 12:18:35 +0100 |
Cezary Kaliszyk |
cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
|
file |
diff |
annotate
|