2014-09-11 blanchet [Thu, 11 Sep 2014 19:18:23 +0200] rev 58307
use new datatypes for benchmarks
src/HOL/Datatype_Benchmark/Brackin.thy src/HOL/Datatype_Benchmark/Instructions.thy

2014-09-11 blanchet [Thu, 11 Sep 2014 18:54:36 +0200] rev 58306
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
src/Doc/Isar_Ref/HOL_Specific.thy src/HOL/Code_Numeral.thy src/HOL/HOLCF/Lift.thy src/HOL/Inductive.thy src/HOL/Library/Bit.thy src/HOL/Library/Extended_Nat.thy src/HOL/Nat.thy src/HOL/Product_Type.thy src/HOL/Sum_Type.thy src/HOL/Tools/Old_Datatype/old_rep_datatype.ML

2014-09-11 blanchet [Thu, 11 Sep 2014 18:54:36 +0200] rev 58305
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
src/Doc/Codegen/Evaluation.thy src/Doc/Codegen/Introduction.thy src/Doc/Codegen/Refinement.thy src/Doc/Datatypes/Datatypes.thy src/Doc/Datatypes/document/root.tex src/Doc/Functions/Functions.thy src/Doc/Isar_Ref/Generic.thy src/Doc/Isar_Ref/HOL_Specific.thy src/Doc/Isar_Ref/Spec.thy src/Doc/Isar_Ref/Synopsis.thy src/Doc/Tutorial/CodeGen/CodeGen.thy src/Doc/Tutorial/Datatype/Fundata.thy src/Doc/Tutorial/Datatype/Nested.thy src/Doc/Tutorial/Protocol/Message.thy src/Doc/Tutorial/Trie/Trie.thy src/HOL/Auth/Event.thy src/HOL/Auth/Guard/Extensions.thy src/HOL/BNF_Examples/Compat.thy src/HOL/BNF_Least_Fixpoint.thy src/HOL/Datatype_Benchmark/Brackin.thy src/HOL/Datatype_Benchmark/Instructions.thy src/HOL/Fun_Def.thy src/HOL/HOLCF/FOCUS/Buffer.thy src/HOL/Hoare/Hoare_Logic.thy src/HOL/Hoare/Hoare_Logic_Abort.thy src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy src/HOL/IMP/Com.thy src/HOL/IMP/Procs.thy src/HOL/Imperative_HOL/Heap.thy src/HOL/Imperative_HOL/ex/Linked_Lists.thy src/HOL/Induct/Com.thy src/HOL/Induct/QuoDataType.thy src/HOL/Induct/QuoNestedDataType.thy src/HOL/Induct/SList.thy src/HOL/Nominal/Examples/Fsub.thy src/HOL/Old_Datatype.thy src/HOL/Quotient_Examples/Quotient_Message.thy src/HOL/SET_Protocol/Event_SET.thy src/HOL/SET_Protocol/Message_SET.thy src/HOL/Tools/BNF/bnf_lfp.ML src/HOL/Tools/Old_Datatype/old_datatype.ML src/HOL/ex/Reflection_Examples.thy src/HOL/ex/Refute_Examples.thy

2014-09-11 blanchet [Thu, 11 Sep 2014 18:54:36 +0200] rev 58304
tuning
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

2014-09-11 blanchet [Thu, 11 Sep 2014 18:54:36 +0200] rev 58303
fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

2014-09-11 blanchet [Thu, 11 Sep 2014 18:54:36 +0200] rev 58302
tuning
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

2014-09-11 blanchet [Thu, 11 Sep 2014 18:54:36 +0200] rev 58301
fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
src/HOL/Library/RBT_Set.thy src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

2014-09-11 blanchet [Thu, 11 Sep 2014 18:54:36 +0200] rev 58300
speed up old Nominal by killing type variables
src/HOL/Nominal/Examples/Type_Preservation.thy src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Tools/BNF/bnf_lfp_compat.ML

2014-09-11 blanchet [Thu, 11 Sep 2014 18:54:36 +0200] rev 58299
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)
src/HOL/ex/Refute_Examples.thy

2014-09-11 blanchet [Thu, 11 Sep 2014 18:54:36 +0200] rev 58298
more docs
src/Doc/Datatypes/Datatypes.thy