2010-12-31 |
Christian Urban |
changed res keyword to set+ for restrictions; comment by a referee
|
file |
diff |
annotate
|
2010-12-28 |
Christian Urban |
automated all strong induction lemmas
|
file |
diff |
annotate
|
2010-12-22 |
Christian Urban |
tuned examples
|
file |
diff |
annotate
|
2010-12-22 |
Christian Urban |
properly exported strong exhaust theorem; cleaned up some examples
|
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-11-14 |
Christian Urban |
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
|
file |
diff |
annotate
|
2010-11-06 |
Christian Urban |
added a test about subtyping; disabled two tests, because of problem with function package
|
file |
diff |
annotate
|
2010-10-14 |
Christian Urban |
major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
|
file |
diff |
annotate
|
2010-09-28 |
Christian Urban |
added Foo1 to explore a contrived example
|
file |
diff |
annotate
|
2010-09-27 |
Christian Urban |
added postprocessed fresh-lemmas for constructors
|
file |
diff |
annotate
|
2010-09-25 |
Christian Urban |
cleaned up two examples
|
file |
diff |
annotate
|
2010-09-20 |
Christian Urban |
introduced a general procedure for structural inductions; simplified reflexivity proof
|
file |
diff |
annotate
|
2010-09-03 |
Christian Urban |
moved a proof to Abs
|
file |
diff |
annotate
|
2010-08-29 |
Christian Urban |
renamed NewParser to Nominal2
|
file |
diff |
annotate
|
2010-08-28 |
Christian Urban |
added fs-instance proofs
|
file |
diff |
annotate
|
2010-08-28 |
Christian Urban |
added proofs for fsupp properties
|
file |
diff |
annotate
|
2010-08-25 |
Christian Urban |
cleaned up (almost completely) the examples
|
file |
diff |
annotate
|
2010-08-25 |
Christian Urban |
automatic lifting
|
file |
diff |
annotate
|
2010-08-21 |
Christian Urban |
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
|
file |
diff |
annotate
|
2010-06-27 |
Christian Urban |
fixed according to changes in quotient
|
file |
diff |
annotate
|
2010-06-02 |
Christian Urban |
fixed problem with bn_info
|
file |
diff |
annotate
|
2010-05-25 |
Cezary Kaliszyk |
Substitution Lemma for TypeSchemes.
|
file |
diff |
annotate
|
2010-05-25 |
Cezary Kaliszyk |
Simplified the proof
|
file |
diff |
annotate
|
2010-05-25 |
Cezary Kaliszyk |
A lemma about substitution in TypeSchemes.
|
file |
diff |
annotate
|
2010-05-12 |
Christian Urban |
fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
|
file |
diff |
annotate
|
2010-05-11 |
Cezary Kaliszyk |
Include raw permutation definitions in eqvt
|
file |
diff |
annotate
|
2010-05-11 |
Cezary Kaliszyk |
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
|
file |
diff |
annotate
|
2010-05-09 |
Christian Urban |
cleaned up a bit the examples; added equivariance to all examples
|
file |
diff |
annotate
|
2010-05-04 |
Cezary Kaliszyk |
Move TypeSchemes to NewParser
|
file |
diff |
annotate
|
2010-04-22 |
Christian Urban |
moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
|
file |
diff |
annotate
|
2010-04-08 |
Christian Urban |
tuned type-schemes example
|
file |
diff |
annotate
|