Nominal/ROOT.ML
2012-01-24 Christian Urban tuned make-file
2011-12-29 Christian Urban separated the two versions of type schemes into two files
2011-12-23 Christian Urban included Pi theory in tests
2011-12-17 Christian Urban updated
2011-12-17 Christian Urban updated in stable branch Nominal2-Isabelle2011-1
2011-12-17 Christian Urban updated all examples in stable branch Nominal2-Isabelle2011-1
2011-11-07 Christian Urban all examples work again after quotient package has been "de-localised"
2011-11-03 Christian Urban updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
2011-06-29 Christian Urban moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
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
2010-08-26 Christian Urban "isabelle make test" makes all major examples....they work up to supp theorems (excluding)
2010-06-23 Christian Urban merged cezary's changes
2010-05-20 Christian Urban new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
2010-05-16 Christian Urban moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
2010-05-14 Christian Urban moved old parser and fv into attic
2010-05-13 Christian Urban added term4 back to the examples
2010-05-12 Christian Urban fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
2010-05-09 Christian Urban tuned file names for examples
2010-05-04 Cezary Kaliszyk "isabelle make" compiles all examples with newparser/newfv/newalpha only.
2010-04-20 Christian Urban renamed Ex1.thy to SingleLet.thy
2010-04-09 Christian Urban renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
2010-04-08 Christian Urban tuned type-schemes example
2010-04-04 Christian Urban separated general nominal theory into separate folder
2010-04-03 Christian Urban added README and moved examples into separate directory
2010-03-26 Cezary Kaliszyk Removed remaining cheats + some cleaning.
2010-03-24 Christian Urban some tuning; possible fix for strange paper generation
2010-03-23 Cezary Kaliszyk More modification needed for compilation
2010-03-17 Christian Urban temporarily disabled tests in Nominal/ROOT
2010-02-25 Cezary Kaliszyk Split Terms into separate files and add them to tests.
2010-02-25 Christian Urban added IsaMakefile...but so far included only a test for the parser
less more (0) tip