2009-03-20 wenzelm [Fri, 20 Mar 2009 15:24:18 +0100] rev 30607
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
doc-src/TutorialI/Protocol/Message.thy doc-src/TutorialI/Protocol/Public.thy src/CCL/Type.thy src/HOL/Auth/Message.thy src/HOL/IMPP/Hoare.thy src/HOL/Modelcheck/mucke_oracle.ML src/HOL/SET-Protocol/Cardholder_Registration.thy src/HOL/SET-Protocol/MessageSET.thy src/HOL/SET-Protocol/PublicSET.thy src/HOL/SET-Protocol/Purchase.thy src/HOL/SizeChange/sct.ML src/HOL/Tools/cnf_funcs.ML src/HOL/Tools/function_package/fundef_core.ML src/HOL/Tools/function_package/mutual.ML src/HOL/Tools/function_package/scnp_reconstruct.ML src/HOL/Tools/function_package/termination.ML src/HOL/Tools/meson.ML src/HOL/Word/WordArith.thy src/HOL/ex/Classical.thy src/HOLCF/IOA/ex/TrivEx.thy src/HOLCF/IOA/ex/TrivEx2.thy src/HOLCF/IOA/meta_theory/Abstraction.thy src/HOLCF/IOA/meta_theory/Sequence.thy src/HOLCF/IOA/meta_theory/Traces.thy src/HOLCF/Lift.thy src/Sequents/LK.thy src/ZF/int_arith.ML

2009-03-20 wenzelm [Fri, 20 Mar 2009 11:26:59 +0100] rev 30606
merged

2009-03-20 berghofe [Fri, 20 Mar 2009 10:44:25 +0100] rev 30605
merged

2009-03-20 berghofe [Fri, 20 Mar 2009 10:43:53 +0100] rev 30604
split_codegen now eta-expands terms on-the-fly.
src/HOL/Product_Type.thy

2009-03-20 wenzelm [Fri, 20 Mar 2009 11:26:25 +0100] rev 30603
proper context for prove_cont/adm_tac;
src/HOLCF/HOLCF.thy src/HOLCF/Tools/adm_tac.ML

2009-03-20 wenzelm [Fri, 20 Mar 2009 11:08:59 +0100] rev 30602
with_attributes: canonical capture/release scheme (potentially iron out race condition);
src/Pure/ML-Systems/multithreading_polyml.ML

2009-03-20 wenzelm [Fri, 20 Mar 2009 09:52:32 +0100] rev 30601
considerable speedup of benchmarks by using minimal simpset;
src/HOL/ex/Lagrange.thy

2009-03-20 wenzelm [Fri, 20 Mar 2009 09:51:41 +0100] rev 30600
allow non-printable symbols within string tokens;
src/Pure/ML/ml_lex.ML

2009-03-19 wenzelm [Thu, 19 Mar 2009 22:05:37 +0100] rev 30599
merged
src/Pure/Isar/antiquote.ML

2009-03-19 huffman [Thu, 19 Mar 2009 08:13:10 -0700] rev 30598
add lemma det_diagonal; remove wellorder requirement on several lemmas
src/HOL/Library/Determinants.thy