2010-12-28 |
Christian Urban |
automated all strong induction lemmas
|
file |
diff |
annotate
|
2010-12-28 |
Christian Urban |
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
|
file |
diff |
annotate
|
2010-12-26 |
Christian Urban |
generated goals for strong induction theorems.
|
file |
diff |
annotate
|
2010-12-23 |
Christian Urban |
moved all strong_exhaust code to nominal_dt_quot; tuned examples
|
file |
diff |
annotate
|
2010-12-21 |
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
|
2010-12-16 |
Christian Urban |
simple cases for strong inducts done; infrastructure for the difficult ones is there
|
file |
diff |
annotate
|
2010-12-14 |
Christian Urban |
freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
|
file |
diff |
annotate
|
2010-12-12 |
Christian Urban |
created strong_exhausts terms
|
file |
diff |
annotate
|
2010-12-12 |
Christian Urban |
moved setify and listify functions into the library; introduced versions that have a type argument
|
file |
diff |
annotate
|
2010-12-08 |
Christian Urban |
first tests about exhaust
|
file |
diff |
annotate
|
2010-12-08 |
Christian Urban |
moved some code into the nominal_library
|
file |
diff |
annotate
|
2010-12-08 |
Christian Urban |
kept the nested structure of constructors (belonging to one datatype)
|
file |
diff |
annotate
|
2010-12-07 |
Christian Urban |
moved general theorems into the libraries
|
file |
diff |
annotate
|
2010-12-07 |
Christian Urban |
automated permute_bn theorems
|
file |
diff |
annotate
|
2010-12-06 |
Christian Urban |
automated alpha_perm_bn theorems
|
file |
diff |
annotate
|
2010-12-06 |
Christian Urban |
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
|
file |
diff |
annotate
|
2010-12-03 |
Christian Urban |
updated to Isabelle 2nd December
|
file |
diff |
annotate
|
2010-11-29 |
Christian Urban |
isarfied some of the high-level proofs
|
file |
diff |
annotate
|
2010-11-29 |
Christian Urban |
added abs_rename_res lemma
|
file |
diff |
annotate
|
2010-11-29 |
Christian Urban |
completed proofs in Foo2
|
file |
diff |
annotate
|
2010-11-28 |
Christian Urban |
completed the strong exhausts rules for Foo2 using general lemmas
|
file |
diff |
annotate
|
2010-11-27 |
Christian Urban |
disabled the Foo examples, because of heavy work
|
file |
diff |
annotate
|
2010-11-26 |
Christian Urban |
slightly simplified the Foo2 tests and hint at a general lemma
|
file |
diff |
annotate
|
2010-11-26 |
Christian Urban |
completely different method fro deriving the exhaust lemma
|
file |
diff |
annotate
|
2010-11-26 |
Cezary Kaliszyk |
missing freshness assumptions
|
file |
diff |
annotate
|
2010-11-25 |
Cezary Kaliszyk |
foo2 strong induction
|
file |
diff |
annotate
|
2010-11-24 |
Cezary Kaliszyk |
foo2 full exhausts
|
file |
diff |
annotate
|
2010-11-24 |
Cezary Kaliszyk |
Foo2 strong_exhaust for first variable.
|
file |
diff |
annotate
|
2010-11-22 |
Cezary Kaliszyk |
single rename in let2
|
file |
diff |
annotate
|
2010-11-21 |
Christian Urban |
added example Foo2.thy
|
file |
diff |
annotate
|