Nominal/nominal_dt_quot.ML
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.
less more (0) -10 -8 tip