2010-08-19 wenzelm [Thu, 19 Aug 2010 18:19:21 +0200] rev 38560
added generated file;
doc-src/Codegen/Thy/document/Evaluation.tex

2010-08-19 wenzelm [Thu, 19 Aug 2010 17:41:52 +0200] rev 38559
merged
NEWS lib/scripts/run-polyml-5.0 src/Pure/ML-Systems/compiler_polyml-5.0.ML src/Pure/ML-Systems/polyml-5.0.ML src/Pure/ML-Systems/polyml-5.1.ML src/Pure/PIDE/markup_node.scala src/Pure/System/isar_document.ML src/Pure/System/isar_document.scala

2010-08-19 haftmann [Thu, 19 Aug 2010 16:08:59 +0200] rev 38558
tuned quotes
src/HOL/Decision_Procs/Approximation.thy src/HOL/Decision_Procs/Cooper.thy src/HOL/Decision_Procs/Ferrack.thy src/HOL/Decision_Procs/MIR.thy src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy src/HOL/Decision_Procs/cooper_tac.ML src/HOL/Decision_Procs/ferrack_tac.ML src/HOL/Decision_Procs/ferrante_rackoff.ML src/HOL/Decision_Procs/langford.ML src/HOL/Decision_Procs/mir_tac.ML src/HOL/Import/shuffler.ML src/HOL/Library/Eval_Witness.thy src/HOL/Library/positivstellensatz.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_inductive2.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/Statespace/distinct_tree_prover.ML src/HOL/Statespace/state_fun.ML src/HOL/Statespace/state_space.ML src/HOL/Tools/Function/function_core.ML src/HOL/Tools/Predicate_Compile/code_prolog.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/Quotient/quotient_term.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/cnf_funcs.ML src/HOL/Tools/groebner.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/prop_logic.ML src/HOL/Tools/sat_funcs.ML src/HOL/Tools/simpdata.ML src/HOL/ex/SVC_Oracle.thy src/HOL/ex/svc_funcs.ML

2010-08-19 haftmann [Thu, 19 Aug 2010 16:08:54 +0200] rev 38557
more antiquotations
src/HOL/Import/proof_kernel.ML src/HOL/Prolog/prolog.ML src/HOL/Tools/Function/termination.ML src/HOL/Tools/meson.ML src/HOLCF/Tools/Domain/domain_library.ML

2010-08-19 haftmann [Thu, 19 Aug 2010 16:08:53 +0200] rev 38556
deglobalized named HOL constants
NEWS src/HOL/Import/HOL/bool.imp src/HOL/Import/HOLLight/hollight.imp src/HOL/Import/hol4rews.ML

2010-08-19 haftmann [Thu, 19 Aug 2010 16:03:07 +0200] rev 38555
deglobalized named HOL constants
src/HOL/HOL.thy src/HOL/Tools/hologic.ML

2010-08-19 haftmann [Thu, 19 Aug 2010 16:03:01 +0200] rev 38554
corrected some long-overseen misperceptions in recdef
src/HOL/Recdef.thy src/HOL/Tools/TFL/dcterm.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/TFL/usyntax.ML

2010-08-19 haftmann [Thu, 19 Aug 2010 12:11:57 +0200] rev 38553
use HOLogic.boolT and @{typ bool} more pervasively
src/HOL/Import/proof_kernel.ML src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML src/HOL/Tools/cnf_funcs.ML src/HOL/Tools/quickcheck_generators.ML src/HOL/Tools/refute.ML

2010-08-19 haftmann [Thu, 19 Aug 2010 11:19:24 +0200] rev 38552
tuned
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

2010-08-19 haftmann [Thu, 19 Aug 2010 11:19:24 +0200] rev 38551
some more antiquotations
src/HOL/Import/hol4rews.ML