2008-03-28 haftmann [Fri, 28 Mar 2008 22:01:56 +0100] rev 26470
unfold_locales now part of default tactic
src/Provers/classical.ML src/Pure/Isar/class.ML

2008-03-28 haftmann [Fri, 28 Mar 2008 22:01:04 +0100] rev 26469
import Main explicitly
src/HOL/ex/Efficient_Nat_examples.thy

2008-03-28 haftmann [Fri, 28 Mar 2008 22:01:03 +0100] rev 26468
dropped now superfluous ad-hoc adaption
src/HOL/ex/Codegenerator_Pretty.thy

2008-03-28 haftmann [Fri, 28 Mar 2008 22:01:02 +0100] rev 26467
not depends on Main any longer
src/HOL/Library/Efficient_Nat.thy

2008-03-28 haftmann [Fri, 28 Mar 2008 22:01:01 +0100] rev 26466
accomodated to sledgehammer theory dependency requirement
src/HOL/Library/Code_Integer.thy

2008-03-28 haftmann [Fri, 28 Mar 2008 22:00:59 +0100] rev 26465
only invoke interpret
src/HOL/Finite_Set.thy

2008-03-28 wenzelm [Fri, 28 Mar 2008 20:08:11 +0100] rev 26464
updated generated file;
doc-src/IsarImplementation/Thy/document/integration.tex

2008-03-28 wenzelm [Fri, 28 Mar 2008 20:02:04 +0100] rev 26463
Context.>> : operate on Context.generic;
doc-src/IsarImplementation/Thy/integration.thy src/Pure/Isar/attrib.ML src/Pure/Isar/calculation.ML src/Pure/Isar/class.ML src/Pure/Isar/code.ML src/Pure/Isar/context_rules.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/locale.ML src/Pure/Isar/method.ML src/Pure/Isar/object_logic.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/rule_insts.ML src/Pure/Isar/skip_proof.ML src/Pure/Proof/extraction.ML src/Pure/Proof/proof_rewrite_rules.ML src/Pure/ProofGeneral/proof_general_emacs.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/Thy/html.ML src/Pure/Thy/term_style.ML src/Pure/Tools/isabelle_process.ML src/Pure/assumption.ML src/Pure/codegen.ML src/Pure/compress.ML src/Pure/context.ML src/Pure/pure_setup.ML src/Pure/pure_thy.ML src/Pure/simplifier.ML

2008-03-28 wenzelm [Fri, 28 Mar 2008 19:43:54 +0100] rev 26462
avoid rebinding of existing facts;
src/HOL/Arith_Tools.thy src/HOL/Groebner_Basis.thy

2008-03-28 haftmann [Fri, 28 Mar 2008 19:12:39 +0100] rev 26461
some styling
doc-src/antiquote_setup.ML