Nominal/Test.thy
2010-03-26 Cezary Kaliszyk Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
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.
less more (0) -50 -30 tip