2009-11-11 wenzelm [Wed, 11 Nov 2009 14:15:11 +0100] rev 33615
uniform use of simultabeous use_thys;
src/CTT/ROOT.ML src/FOL/ROOT.ML src/FOLP/ROOT.ML src/HOL/Bali/ROOT.ML src/HOL/Boogie/ROOT.ML src/HOL/Decision_Procs/ROOT.ML src/HOL/Hahn_Banach/ROOT.ML src/HOL/Hoare_Parallel/ROOT.ML src/HOL/IMPP/ROOT.ML src/HOL/IOA/ROOT.ML src/HOL/Imperative_HOL/ROOT.ML src/HOL/Induct/ROOT.ML src/HOL/Lambda/ROOT.ML src/HOL/Lattice/ROOT.ML src/HOL/MicroJava/ROOT.ML src/HOL/Mirabelle/ROOT.ML src/HOL/Multivariate_Analysis/ROOT.ML src/HOL/NSA/Examples/ROOT.ML src/HOL/NSA/ROOT.ML src/HOL/NanoJava/ROOT.ML src/HOL/Nominal/Examples/ROOT.ML src/HOL/Nominal/ROOT.ML src/HOL/Number_Theory/ROOT.ML src/HOL/Probability/ROOT.ML src/HOL/ROOT.ML src/HOL/SET_Protocol/ROOT.ML src/HOL/SMT/Examples/ROOT.ML src/HOL/SMT/ROOT.ML src/HOL/Statespace/ROOT.ML src/HOL/Subst/ROOT.ML src/HOL/TLA/Buffer/ROOT.ML src/HOL/TLA/Inc/ROOT.ML src/HOL/TLA/Memory/ROOT.ML src/HOL/TLA/ROOT.ML src/HOL/UNITY/ROOT.ML src/HOL/Unix/ROOT.ML src/HOL/W0/ROOT.ML src/HOL/Word/Examples/ROOT.ML src/HOL/Word/ROOT.ML src/HOL/ZF/ROOT.ML src/HOL/base.ML src/HOL/main.ML src/HOL/plain.ML src/HOLCF/IOA/ABP/ROOT.ML src/HOLCF/IOA/NTP/ROOT.ML src/HOLCF/IOA/ROOT.ML src/HOLCF/IOA/Storage/ROOT.ML src/HOLCF/IOA/ex/ROOT.ML src/HOLCF/ROOT.ML src/LCF/ROOT.ML ...

2009-11-11 haftmann [Wed, 11 Nov 2009 16:19:28 +0100] rev 33614
merged

2009-11-11 haftmann [Wed, 11 Nov 2009 15:10:29 +0100] rev 33613
explicit invocation of code generation
src/HOL/ex/Records.thy

2009-11-11 haftmann [Wed, 11 Nov 2009 15:10:26 +0100] rev 33612
adding code equations for constructors
src/HOL/Tools/record.ML

2009-11-11 haftmann [Wed, 11 Nov 2009 10:06:30 +0100] rev 33611
tuned
src/HOL/Tools/Function/function_lib.ML

2009-11-11 boehmes [Wed, 11 Nov 2009 15:43:03 +0100] rev 33610
changed URL of SMT server,
added Z3 rewrite lemma
src/HOL/SMT/Z3.thy src/HOL/SMT/etc/settings

2009-11-11 paulson [Wed, 11 Nov 2009 14:04:56 +0000] rev 33609
Added two new lemmas
src/HOL/SupInf.thy

2009-11-11 haftmann [Wed, 11 Nov 2009 09:02:37 +0100] rev 33608
tuned imports
src/HOL/Nitpick.thy

2009-11-11 haftmann [Wed, 11 Nov 2009 09:02:20 +0100] rev 33607
tuned
src/HOL/Predicate.thy

2009-11-11 wenzelm [Wed, 11 Nov 2009 00:11:26 +0100] rev 33606
local mutex for theory content/identity operations;
src/Pure/context.ML