2005-06-17 wenzelm [Fri, 17 Jun 2005 18:36:25 +0200] rev 16459
updated;
doc-src/IsarOverview/Isar/document/Induction.tex doc-src/IsarOverview/Isar/document/Logic.tex

2005-06-17 wenzelm [Fri, 17 Jun 2005 18:35:27 +0200] rev 16458
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
src/HOL/Tools/recdef_package.ML src/HOL/Tools/record_package.ML src/HOL/Tools/typedef_package.ML src/Provers/Arith/fast_lin_arith.ML src/Pure/Isar/attrib.ML src/Pure/Isar/locale.ML src/Pure/Isar/proof_context.ML src/Pure/Proof/extraction.ML src/Pure/axclass.ML src/Pure/codegen.ML src/Pure/goals.ML src/Pure/meta_simplifier.ML src/Pure/proofterm.ML src/Pure/simplifier.ML src/Sequents/prover.ML src/ZF/Tools/induct_tacs.ML src/ZF/Tools/typechk.ML

2005-06-17 wenzelm [Fri, 17 Jun 2005 18:33:42 +0200] rev 16457
Context.names_of;
src/ZF/Tools/inductive_package.ML

2005-06-17 wenzelm [Fri, 17 Jun 2005 18:33:41 +0200] rev 16456
* Pure/TheoryDataFun: change of the argument structure;
* Pure/TheoryDataFun: change of the argument structure -- got rid of Sign.sg;
NEWS

2005-06-17 wenzelm [Fri, 17 Jun 2005 18:33:40 +0200] rev 16455
Sign.root_path, Sign.local_path;
src/Pure/Thy/thy_parse.ML

2005-06-17 wenzelm [Fri, 17 Jun 2005 18:33:39 +0200] rev 16454
removed obsolete theory_of_sign, theory_of_thm;
Context.draftN;
Context.begin_theory;
src/Pure/Thy/thy_info.ML

2005-06-17 wenzelm [Fri, 17 Jun 2005 18:33:38 +0200] rev 16453
PolyML.Compiler.printInAlphabeticalOrder := false;
src/Pure/ML-Systems/polyml.ML

2005-06-17 wenzelm [Fri, 17 Jun 2005 18:33:37 +0200] rev 16452
Context.DATA_FAIL;
accomodate identification of type Sign.sg and theory;
src/Pure/Isar/toplevel.ML

2005-06-17 wenzelm [Fri, 17 Jun 2005 18:33:36 +0200] rev 16451
Context.PureN;
src/Pure/Isar/session.ML

2005-06-17 wenzelm [Fri, 17 Jun 2005 18:33:35 +0200] rev 16450
RuleCases.tactic;
accomodate identification of type Sign.sg and theory;
src/Pure/Isar/proof.ML