2014-09-11 blanchet 2014-09-11 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-09-11 blanchet 2014-09-11 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
2014-09-11 blanchet 2014-09-11 tuning
2014-09-11 blanchet 2014-09-11 fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
2014-09-11 blanchet 2014-09-11 tuning
2014-09-11 blanchet 2014-09-11 fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
2014-09-11 blanchet 2014-09-11 speed up old Nominal by killing type variables
2014-09-11 blanchet 2014-09-11 took out some datatype tests for Refute -- these yield timeouts on some Isatests after transition to new datatypes, for some reason (and Refute is obsolete anyway)
2014-09-11 blanchet 2014-09-11 more docs
2014-09-11 traytel 2014-09-11 new deads go to the end
2014-09-11 blanchet 2014-09-11 comment
2014-09-10 haftmann 2014-09-10 more material on lists
2014-09-10 haftmann 2014-09-10 explicit check phase to guide type inference of class expression towards one single type variable
2014-09-10 haftmann 2014-09-10 tuned
2014-09-10 haftmann 2014-09-10 dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns
2014-09-09 blanchet 2014-09-09 tuning
2014-09-09 blanchet 2014-09-09 proper checks -- the calls data structure may contain spurious entries
2014-09-09 blanchet 2014-09-09 avoid exception
2014-09-09 blanchet 2014-09-09 avoid internal fact
2014-09-09 blanchet 2014-09-09 restored old case names
2014-09-09 blanchet 2014-09-09 compile
2014-09-09 blanchet 2014-09-09 avoid duplicate case names
2014-09-09 blanchet 2014-09-09 nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
2014-09-09 blanchet 2014-09-09 preserve case names in '(co)induct' theorems generated by prim(co)rec'
2014-09-09 blanchet 2014-09-09 hide DEADID/ID theorems
2014-09-09 blanchet 2014-09-09 tuning
2014-09-09 blanchet 2014-09-09 more canonical (and correct) local theory threading
2014-09-09 blanchet 2014-09-09 removed 'datatype_compat's that are no longer needed
2014-09-09 blanchet 2014-09-09 documented extraction plugin
2014-09-09 blanchet 2014-09-09 made realizer more robust in the face of nesting through functions
2014-09-09 blanchet 2014-09-09 removed debugging junk
2014-09-09 blanchet 2014-09-09 renamed ML file and module
2014-09-09 blanchet 2014-09-09 made datatype realizer plugin work for new-style datatypes with no nesting
2014-09-09 blanchet 2014-09-09 ported HOL-Proofs-Lambda to new datatypes
2014-09-09 blanchet 2014-09-09 ported HOL-Proofs-Extraction to new datatypes
2014-09-09 blanchet 2014-09-09 made SML/NJ happier
2014-09-09 blanchet 2014-09-09 more porting to new datatypes
2014-09-09 blanchet 2014-09-09 tuned IArray code generator w.r.t. map rel set
2014-09-09 blanchet 2014-09-09 ported Nitpick_Examples to new datatypes
2014-09-09 blanchet 2014-09-09 set 'fundef_cong' attribute also for (co)datatypes with no live type variables
2014-09-09 blanchet 2014-09-09 ported IArray to new datatypes
2014-09-09 blanchet 2014-09-09 prevent infinite loop when type variables are of a non-'type' sort
2014-09-09 blanchet 2014-09-09 tuned code
2014-09-09 blanchet 2014-09-09 ported MicroJava to new datatypes
2014-09-09 blanchet 2014-09-09 rename_tac'd scrips
2014-09-09 blanchet 2014-09-09 ported Unix to new datatypes
2014-09-09 blanchet 2014-09-09 ported Isar_Examples to new datatypes
2014-09-09 blanchet 2014-09-09 ported Decision_Procs to new datatypes
2014-09-09 blanchet 2014-09-09 ported Induct to new datatypes
2014-09-09 blanchet 2014-09-09 half-ported Imperative HOL to new datatypes
2014-09-09 blanchet 2014-09-09 generalized 'datatype' LaTeX antiquotation and added 'codatatype'
2014-09-09 blanchet 2014-09-09 tuned messages
2014-09-09 blanchet 2014-09-09 rename_tac'd scripts
2014-09-09 blanchet 2014-09-09 reverted 83a8570b44bc, which was a misunderstanding
2014-09-09 blanchet 2014-09-09 rename_tac'd script
2014-09-09 blanchet 2014-09-09 ported Bali to new datatypes
2014-09-09 blanchet 2014-09-09 rename_tac'd scripts
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-09-09 nipkow 2014-09-09 merged
2014-09-09 nipkow 2014-09-09 enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc