Nominal/ROOT.ML
2011-02-28 Christian Urban included old test cases for perm_simp into ROOT.ML file
2011-01-06 Christian Urban moved Weakening up....it does not compile when put at the last position
2011-01-06 Christian Urban added weakening to the test cases
2010-12-23 Christian Urban moved all strong_exhaust code to nominal_dt_quot; tuned examples
2010-12-22 Christian Urban corrected premises of strong exhausts theorems
2010-12-22 Christian Urban properly exported strong exhaust theorem; cleaned up some examples
2010-11-27 Christian Urban disabled the Foo examples, because of heavy work
2010-11-24 Christian Urban added example from the F-ing paper by Rossberg, Russo and Dreyer
2010-11-15 Christian Urban added a test for the various shallow binders
2010-11-14 Christian Urban merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
2010-11-06 Christian Urban added a test about subtyping; disabled two tests, because of problem with function package
2010-09-28 Christian Urban added Foo1 to explore a contrived example
2010-09-22 Christian Urban fixed
2010-09-22 Christian Urban made supp proofs more robust by not using the standard induction; renamed some example files
2010-08-29 Christian Urban renamed NewParser to Nominal2
less more (0) -15 tip