Nominal/nominal_dt_quot.ML
2012-05-22 Cezary Kaliszyk Added workaround for broken quotient_type in tip isabelle.
2012-04-20 Cezary Kaliszyk Pass proper rsp theorems for constructors and for size
2012-04-10 Christian Urban moved lift_raw_const from Quotient to Nominal
2012-04-10 Christian Urban updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)
2011-12-05 Christian Urban tiny improvement by removing one unnecessary assumption
2011-11-30 Christian Urban updated to changes in the quotient package (patch by Ondrej Kuncar)
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-04-13 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
2011-01-04 Christian Urban final version of the ESOP paper; used set+ instead of res as requested by one reviewer
2011-01-03 Christian Urban simple cases for string rule inductions
2010-12-28 Christian Urban automated all strong induction lemmas
2010-12-28 Christian Urban proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
2010-12-26 Christian Urban generated goals for strong induction theorems.
2010-12-23 Christian Urban moved all strong_exhaust code to nominal_dt_quot; tuned examples
2010-12-07 Christian Urban automated permute_bn theorems
2010-12-06 Christian Urban moved code from nominal_dt_supp to nominal_dt_quot
2010-11-22 Cezary Kaliszyk current isabelle
2010-09-10 Christian Urban tuned (to conform with indentation policy of Markus)
2010-09-10 Christian Urban supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
2010-08-25 Christian Urban automatic lifting
2010-08-25 Christian Urban everything now lifts as expected
2010-08-25 Christian Urban now every lemma lifts (even with type variables)
2010-08-25 Christian Urban can now deal with type variables in nominal datatype definitions
2010-08-22 Christian Urban updated to new Isabelle
2010-08-22 Christian Urban updated to new Isabelle
2010-08-21 Christian Urban moved lifting code from Lift.thy to nominal_dt_quot.ML
2010-08-16 Christian Urban modified the code for class instantiations (with help from Florian)
2010-08-15 Christian Urban defined qperms and qsizes
2010-08-14 Christian Urban improved code
less more (0) -30 tip