2006-01-03 wenzelm [Tue, 03 Jan 2006 00:06:18 +0100] rev 18540
* Pure/Isar: new command 'unfolding';
* ML/Provers: more generic wrt. syntax of object-logics;
tuned;
NEWS

2006-01-02 wenzelm [Mon, 02 Jan 2006 20:50:17 +0100] rev 18539
ISABELLE_USER for remote cvs access;
Admin/makedist

2006-01-02 wenzelm [Mon, 02 Jan 2006 20:42:12 +0100] rev 18538
outline;
doc-src/IsarImplementation/Thy/ML.thy

2006-01-02 wenzelm [Mon, 02 Jan 2006 20:16:52 +0100] rev 18537
"The Isabelle/Isar Implementation" manual;
doc-src/IsarImplementation/IsaMakefile doc-src/IsarImplementation/Makefile doc-src/IsarImplementation/Thy/ML.thy doc-src/IsarImplementation/Thy/ROOT.ML doc-src/IsarImplementation/Thy/base.thy doc-src/IsarImplementation/Thy/document/ML.tex doc-src/IsarImplementation/Thy/document/base.tex doc-src/IsarImplementation/Thy/document/integration.tex doc-src/IsarImplementation/Thy/document/locale.tex doc-src/IsarImplementation/Thy/document/logic.tex doc-src/IsarImplementation/Thy/document/prelim.tex doc-src/IsarImplementation/Thy/document/proof.tex doc-src/IsarImplementation/Thy/document/session.tex doc-src/IsarImplementation/Thy/document/tactic.tex doc-src/IsarImplementation/Thy/integration.thy doc-src/IsarImplementation/Thy/locale.thy doc-src/IsarImplementation/Thy/logic.thy doc-src/IsarImplementation/Thy/prelim.thy doc-src/IsarImplementation/Thy/proof.thy doc-src/IsarImplementation/Thy/setup.ML doc-src/IsarImplementation/Thy/tactic.thy doc-src/IsarImplementation/Thy/unused.thy doc-src/IsarImplementation/checkglossary doc-src/IsarImplementation/implementation.tex doc-src/IsarImplementation/intro.tex doc-src/IsarImplementation/makeglossary doc-src/IsarImplementation/style.sty

2005-12-31 wenzelm [Sat, 31 Dec 2005 21:49:44 +0100] rev 18536
* Provers/classical: removed obsolete classical version of elim_format;
NEWS

2005-12-31 wenzelm [Sat, 31 Dec 2005 21:49:43 +0100] rev 18535
tuned forall_intr_vars;
src/Pure/drule.ML

2005-12-31 wenzelm [Sat, 31 Dec 2005 21:49:42 +0100] rev 18534
added classical_rule, which replaces Data.make_elim;
removed obsolete Data.make_elim and classical elim_format attribute;
tuned;
src/Provers/classical.ML

2005-12-31 wenzelm [Sat, 31 Dec 2005 21:49:41 +0100] rev 18533
explicitly reject consts *Goal*, *False*;
src/Provers/blast.ML

2005-12-31 wenzelm [Sat, 31 Dec 2005 21:49:40 +0100] rev 18532
elim rules: Classical.classical_rule;
src/HOL/Tools/res_axioms.ML

2005-12-31 wenzelm [Sat, 31 Dec 2005 21:49:39 +0100] rev 18531
removed obsolete cla_dist_concl;
src/FOL/FOL.thy src/HOL/HOL.thy