src/HOL/Nominal/nominal_primrec.ML
2007-04-15 wenzelm 2007-04-15 removed obsolete TypeInfer.logicT -- use dummyT;
2007-04-15 wenzelm 2007-04-15 proper ProofContext.infer_types;
2007-03-10 berghofe 2007-03-10 - Replaced fold by fold_rev to make sure that list of predicate variables pvars (for invariants) is in the correct order - Adapted to new format of datatype descriptor
2007-02-16 berghofe 2007-02-16 Replaced "raise RecError" by "primrec_err" in function gen_primrec_i to prevent error message from being suppressed.
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse;
2006-12-11 berghofe 2006-12-11 nominal_primrec now prints initial proof state.
2006-12-01 nipkow 2006-12-01 Added missing "standard"
2006-11-27 berghofe 2006-11-27 Implemented new "nominal_primrec" command for defining functions on nominal datatypes.