2006-01-21 wenzelm [Sat, 21 Jan 2006 23:02:14 +0100] rev 18728
simplified type attribute;
src/HOL/Import/hol4rews.ML src/HOL/Import/proof_kernel.ML src/HOL/Import/shuffler.ML src/HOL/Tools/datatype_abs_proofs.ML src/HOL/Tools/datatype_aux.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/datatype_rep_proofs.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/primrec_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/recfun_codegen.ML src/HOL/Tools/record_package.ML src/HOL/Tools/res_axioms.ML src/HOL/Tools/split_rule.ML src/HOL/Tools/typedef_package.ML src/HOL/arith_data.ML src/HOLCF/domain/theorems.ML src/HOLCF/fixrec_package.ML src/HOLCF/pcpodef_package.ML src/Provers/clasimp.ML src/Provers/classical.ML src/Provers/splitter.ML src/Pure/Isar/args.ML src/Pure/Isar/calculation.ML src/Pure/Isar/constdefs.ML src/Pure/Isar/context_rules.ML src/Pure/Isar/induct_attrib.ML src/Pure/Isar/isar_thy.ML src/Pure/Isar/locale.ML src/Pure/Isar/method.ML src/Pure/Isar/object_logic.ML src/Pure/Isar/obtain.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/rule_cases.ML src/Pure/Isar/specification.ML src/Pure/Proof/extraction.ML src/Pure/Tools/class_package.ML src/Pure/axclass.ML src/Pure/codegen.ML src/Pure/pure_thy.ML src/Pure/simplifier.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/ind_cases.ML src/ZF/Tools/induct_tacs.ML src/ZF/Tools/inductive_package.ML src/ZF/Tools/primrec_package.ML

2006-01-20 mengj [Fri, 20 Jan 2006 04:53:59 +0100] rev 18727
type information is now also printed.
src/HOL/Tools/res_atp_setup.ML

2006-01-20 mengj [Fri, 20 Jan 2006 04:50:01 +0100] rev 18726
added some debugging code.
src/HOL/Tools/res_atp_provers.ML

2006-01-20 mengj [Fri, 20 Jan 2006 04:35:23 +0100] rev 18725
fixed a bug
src/HOL/Tools/res_hol_clause.ML

2006-01-19 wenzelm [Thu, 19 Jan 2006 21:22:30 +0100] rev 18724
quote "atom";
doc-src/TutorialI/CTL/Base.thy doc-src/TutorialI/CTL/CTL.thy doc-src/TutorialI/CTL/PDL.thy doc-src/TutorialI/CTL/document/PDL.tex

2006-01-19 wenzelm [Thu, 19 Jan 2006 21:22:29 +0100] rev 18723
updated;
doc-src/LaTeXsugar/Sugar/document/Sugar.tex doc-src/TutorialI/CTL/document/Base.tex

2006-01-19 wenzelm [Thu, 19 Jan 2006 21:22:27 +0100] rev 18722
* ML/Isar: theory setup has type (theory -> theory);
NEWS

2006-01-19 wenzelm [Thu, 19 Jan 2006 21:22:26 +0100] rev 18721
use/use_thy: Output.toplevel_errors;
src/Pure/Thy/thy_info.ML

2006-01-19 wenzelm [Thu, 19 Jan 2006 21:22:25 +0100] rev 18720
added basic syntax;
removed pure syntax;
src/Pure/Syntax/syntax.ML

2006-01-19 wenzelm [Thu, 19 Jan 2006 21:22:24 +0100] rev 18719
moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
src/Pure/Syntax/mixfix.ML