| Tue, 28 Dec 2010 00:20:50 +0000 |
Christian Urban |
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
|
file |
diff |
annotate
|
| Sun, 26 Dec 2010 16:35:16 +0000 |
Christian Urban |
generated goals for strong induction theorems.
|
file |
diff |
annotate
|
| Thu, 23 Dec 2010 00:46:06 +0000 |
Christian Urban |
moved all strong_exhaust code to nominal_dt_quot; tuned examples
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 14:27:39 +0000 |
Christian Urban |
automated permute_bn theorems
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 17:11:34 +0000 |
Christian Urban |
moved code from nominal_dt_supp to nominal_dt_quot
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 16:14:47 +0900 |
Cezary Kaliszyk |
current isabelle
|
file |
diff |
annotate
|
| Sat, 11 Sep 2010 05:56:49 +0800 |
Christian Urban |
tuned (to conform with indentation policy of Markus)
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 09:17:40 +0800 |
Christian Urban |
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 22:55:42 +0800 |
Christian Urban |
automatic lifting
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 20:19:10 +0800 |
Christian Urban |
everything now lifts as expected
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 11:58:37 +0800 |
Christian Urban |
now every lemma lifts (even with type variables)
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:02:06 +0800 |
Christian Urban |
can now deal with type variables in nominal datatype definitions
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 14:02:49 +0800 |
Christian Urban |
updated to new Isabelle
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 11:00:53 +0800 |
Christian Urban |
updated to new Isabelle
|
file |
diff |
annotate
|
| Sat, 21 Aug 2010 20:07:36 +0800 |
Christian Urban |
moved lifting code from Lift.thy to nominal_dt_quot.ML
|
file |
diff |
annotate
|
| Mon, 16 Aug 2010 17:39:16 +0800 |
Christian Urban |
modified the code for class instantiations (with help from Florian)
|
file |
diff |
annotate
|