2010-03-07 wenzelm [Sun, 07 Mar 2010 12:19:47 +0100] rev 35625
modernized structure Object_Logic;
src/HOL/Boogie/Tools/boogie_loader.ML 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/mir_tac.ML src/HOL/HOL.thy src/HOL/Library/Efficient_Nat.thy src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML src/HOL/Library/normarith.ML src/HOL/Mutabelle/mutabelle.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/NSA/transfer.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/datatype_abs_proofs.ML src/HOL/Tools/Datatype/datatype_realizer.ML src/HOL/Tools/Function/induction_schema.ML src/HOL/Tools/Function/termination.ML src/HOL/Tools/Groebner_Basis/groebner.ML src/HOL/Tools/Nitpick/minipick.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_model.ML src/HOL/Tools/Qelim/ferrante_rackoff.ML src/HOL/Tools/Qelim/langford.ML src/HOL/Tools/Qelim/presburger.ML src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/TFL/post.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/hologic.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/meson.ML src/HOL/Tools/record.ML src/HOL/Tools/res_axioms.ML src/HOL/Tools/sat_funcs.ML src/HOL/Tools/typedef.ML src/Provers/blast.ML src/Provers/classical.ML src/Provers/splitter.ML src/Pure/Isar/attrib.ML src/Pure/Isar/auto_bind.ML src/Pure/Isar/element.ML src/Pure/Isar/expression.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/method.ML src/Pure/Isar/object_logic.ML src/Pure/Isar/obtain.ML src/Pure/Isar/rule_cases.ML src/Pure/Isar/specification.ML ...

2010-03-07 wenzelm [Sun, 07 Mar 2010 11:57:16 +0100] rev 35624
modernized structure Local_Defs;
src/HOL/Library/reflection.ML src/HOL/NSA/transfer.ML src/HOL/Tools/Function/mutual.ML src/HOL/Tools/Function/scnp_reconstruct.ML src/HOL/Tools/Groebner_Basis/normalizer_data.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/HOL/Tools/Quotient/quotient_def.ML src/HOL/Tools/inductive.ML src/HOL/Tools/res_axioms.ML src/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOLCF/Tools/fixrec.ML src/Pure/Isar/attrib.ML src/Pure/Isar/code.ML src/Pure/Isar/constdefs.ML src/Pure/Isar/element.ML src/Pure/Isar/expression.ML src/Pure/Isar/local_defs.ML src/Pure/Isar/method.ML src/Pure/Isar/proof.ML src/Pure/Isar/specification.ML src/Pure/Isar/theory_target.ML src/Tools/Code/code_preproc.ML src/Tools/induct.ML

2010-03-06 paulson [Sat, 06 Mar 2010 19:17:59 +0000] rev 35623
merged

2010-03-06 paulson [Sat, 06 Mar 2010 17:21:59 +0000] rev 35622
merged

2010-03-06 paulson [Sat, 06 Mar 2010 17:19:29 +0000] rev 35621
simplified
src/HOL/Induct/Comb.thy

2010-03-06 haftmann [Sat, 06 Mar 2010 20:16:31 +0100] rev 35620
merged

2010-03-06 haftmann [Sat, 06 Mar 2010 15:31:31 +0100] rev 35619
lemma restrict_complement_singleton_eq
src/HOL/Map.thy

2010-03-06 haftmann [Sat, 06 Mar 2010 15:31:30 +0100] rev 35618
some lemma refinements
src/HOL/Library/RBT.thy

2010-03-06 haftmann [Sat, 06 Mar 2010 15:31:30 +0100] rev 35617
added Table.thy
src/HOL/IsaMakefile src/HOL/Library/Library.thy src/HOL/Library/Table.thy src/HOL/ex/Codegenerator_Candidates.thy

2010-03-06 wenzelm [Sat, 06 Mar 2010 17:53:04 +0100] rev 35616
provide ProofContext.def_type depending on "pattern" mode;
src/Pure/Isar/proof_context.ML