2009-06-05 haftmann [Fri, 05 Jun 2009 09:23:41 +0200] rev 31463
added mk_valtermify_app and mk_random
src/HOL/Tools/hologic.ML

2009-06-05 haftmann [Fri, 05 Jun 2009 08:28:24 +0200] rev 31462
Set.insert with authentic syntax
src/HOL/Library/LaTeXsugar.thy

2009-06-05 haftmann [Fri, 05 Jun 2009 08:06:03 +0200] rev 31461
merged
src/HOL/Finite_Set.thy src/HOL/Set.thy src/Pure/Concurrent/ROOT.ML src/Pure/General/ROOT.ML src/Pure/Isar/ROOT.ML src/Pure/ML-Systems/install_pp_polyml-experimental.ML src/Pure/ProofGeneral/ROOT.ML src/Pure/Tools/ROOT.ML

2009-06-05 haftmann [Fri, 05 Jun 2009 08:00:53 +0200] rev 31460
Set.insert with authentic syntax
src/HOL/TLA/Intensional.thy

2009-06-04 haftmann [Thu, 04 Jun 2009 16:55:20 +0200] rev 31459
added trees implementing mappings
src/HOL/IsaMakefile src/HOL/Library/Mapping.thy src/HOL/Library/Tree.thy src/HOL/ex/Codegenerator_Candidates.thy

2009-06-04 haftmann [Thu, 04 Jun 2009 16:11:04 +0200] rev 31458
avoid Library.foldl_map
src/HOL/Nominal/nominal_package.ML src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/datatype_realizer.ML src/HOL/Tools/inductive_realizer.ML

2009-06-04 haftmann [Thu, 04 Jun 2009 16:11:03 +0200] rev 31457
class replaces axclass
src/HOL/Library/Topology_Euclidean_Space.thy

2009-06-04 haftmann [Thu, 04 Jun 2009 15:28:59 +0200] rev 31456
insert now qualified and with authentic syntax
src/HOL/Set.thy src/HOL/Tools/hologic.ML

2009-06-04 haftmann [Thu, 04 Jun 2009 15:28:59 +0200] rev 31455
lemma about List.foldl and Finite_Set.fold
src/HOL/List.thy

2009-06-04 haftmann [Thu, 04 Jun 2009 15:28:58 +0200] rev 31454
dropped legacy ML bindings; tuned
src/HOL/Hilbert_Choice.thy src/HOL/Tools/meson.ML src/HOL/Tools/res_axioms.ML