Nominal/Test.thy
2010-03-24 Christian Urban some tuning; possible fix for strange paper generation
2010-03-23 Cezary Kaliszyk More reorganization.
2010-03-23 Cezary Kaliszyk Move Leroy out of Test, rename accordingly.
2010-03-23 Cezary Kaliszyk Term1 is identical to Example 3
2010-03-23 Cezary Kaliszyk Move example3 out.
2010-03-23 Cezary Kaliszyk Move Ex1 and Ex2 out of Test
2010-03-23 Cezary Kaliszyk Move examples which create more permutations out
2010-03-23 Cezary Kaliszyk Move LamEx out of Test.
2010-03-23 Cezary Kaliszyk Move Non-respectful examples to NotRsp
2010-03-23 Cezary Kaliszyk Move the comment to appropriate place.
2010-03-19 Cezary Kaliszyk Automatically derive support for datatypes with at-most one binding per constructor.
2010-03-19 Cezary Kaliszyk Update Test to use fset.
2010-03-18 Cezary Kaliszyk Leroy96 supp=fv and fixes to make it compile
2010-03-18 Christian Urban corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
2010-03-18 Cezary Kaliszyk Rename "_property" to ".property"
2010-03-18 Cezary Kaliszyk Added fv,bn,distinct,perm to the simplifier.
2010-03-18 Cezary Kaliszyk Which proofs need a 'sorry'.
2010-03-18 Christian Urban vixed variable names
2010-03-18 Christian Urban simplified strong induction proof by using flip
2010-03-18 Cezary Kaliszyk Rename bound variables + minor cleaning.
2010-03-18 Cezary Kaliszyk Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
2010-03-17 Christian Urban merged
2010-03-17 Christian Urban added partial proof for the strong induction principle
2010-03-17 Cezary Kaliszyk merge
2010-03-17 Cezary Kaliszyk cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
2010-03-17 Christian Urban added proof of supp/fv for type schemes
2010-03-17 Christian Urban added partial proof of supp for type schemes
2010-03-17 Cezary Kaliszyk Fix in alpha; support of the recursive Let works :)
2010-03-17 Cezary Kaliszyk The recursive supp just has one equation too much.
2010-03-17 Christian Urban commented out examples that should not work; but for example type-scheme example should work
2010-03-17 Christian Urban added another supp-proof for the non-recursive case
2010-03-16 Christian Urban added the final unfolded result
2010-03-16 Christian Urban merge and proof of support for non-recursive case
2010-03-16 Cezary Kaliszyk alpha_bn doesn't need the permutation in non-recursive case.
2010-03-16 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings.
2010-03-16 Cezary Kaliszyk The proof in 'Test' gets simpler.
2010-03-15 Christian Urban merged (confirmed to work with Isabelle from 6th March)
2010-03-15 Christian Urban proof for support when bn-function is present, but fb_function is empty
2010-03-15 Cezary Kaliszyk fv_eqvt_cheat no longer needed.
2010-03-15 Cezary Kaliszyk derive "inducts" from "induct" instead of lifting again is much faster.
2010-03-15 Cezary Kaliszyk cheat_alpha_eqvt no longer needed; the proofs work.
2010-03-15 Cezary Kaliszyk Use eqvt.
2010-03-15 Christian Urban added an eqvt-proof for bi
2010-03-13 Christian Urban started supp-fv proofs (is going to work)
2010-03-11 Cezary Kaliszyk Show that the new types are in finite support typeclass.
2010-03-11 Cezary Kaliszyk With the 4 cheats, all examples fully lift.
2010-03-11 Cezary Kaliszyk Lifting constants.
2010-03-10 Cezary Kaliszyk Reordered examples in Test.
2010-03-10 Cezary Kaliszyk Linked parser to fv and alpha.
2010-03-10 Christian Urban parser produces ordered bn-fun information
2010-03-09 Christian Urban added bn-information, but it is not yet ordered according to the dts
2010-03-09 Cezary Kaliszyk All examples should work.
2010-03-08 Christian Urban added a test-file for compatibility
2010-03-08 Christian Urban added compat definitions to some examples
2010-03-08 Christian Urban deleted comments about "weird"
2010-03-08 Cezary Kaliszyk With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
2010-03-07 Christian Urban merged
2010-03-04 Christian Urban merged
2010-03-04 Christian Urban merged
2010-03-04 Christian Urban more proofs in Abs and work on Core Haskell
less more (0) -60 tip