2004-04-02 ballarin [Fri, 02 Apr 2004 14:08:30 +0200] rev 14508
Experimental command for instantiation of locales in proof contexts:
instantiate <label>: <loc>
NEWS etc/isar-keywords-ZF.el etc/isar-keywords.el src/FOL/IsaMakefile src/FOL/ex/LocaleInst.thy src/Pure/Isar/isar_syn.ML src/Pure/Isar/isar_thy.ML src/Pure/Isar/locale.ML src/Pure/Isar/method.ML src/Pure/Isar/outer_parse.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML

2004-04-02 nipkow [Fri, 02 Apr 2004 12:25:48 +0200] rev 14507
ignore_neq also influences arith_tac now, not just fast_arith_tac
src/HOL/arith_data.ML

2004-04-02 nipkow [Fri, 02 Apr 2004 12:08:38 +0200] rev 14506
Added ignore_neq flag.
src/HOL/arith_data.ML

2004-04-01 paulson [Thu, 01 Apr 2004 15:05:04 +0200] rev 14505
removal of Binary Trees examples prepratory to its going into AFP
src/HOL/Induct/BinaryTree.thy src/HOL/Induct/BinaryTree_Map.thy src/HOL/Induct/BinaryTree_TacticStyle.thy src/HOL/Induct/ROOT.ML src/HOL/IsaMakefile

2004-04-01 paulson [Thu, 01 Apr 2004 10:54:32 +0200] rev 14504
new type class abelian_group
src/HOL/Finite_Set.thy src/HOL/Ring_and_Field.thy

2004-03-31 skalberg [Wed, 31 Mar 2004 16:10:53 +0200] rev 14503
Added check that Theory.ML does not occur in the files section of the theory
Theory.
NEWS src/Pure/Isar/isar_thy.ML

2004-03-31 nipkow [Wed, 31 Mar 2004 11:02:00 +0200] rev 14502
Lex now in AFP
src/HOL/IsaMakefile

2004-03-31 nipkow [Wed, 31 Mar 2004 11:00:25 +0200] rev 14501
HOL/Lex is now in AFP/Functional-Automata
src/HOL/Lex/AutoChopper.thy src/HOL/Lex/AutoChopper1.thy src/HOL/Lex/AutoMaxChop.thy src/HOL/Lex/AutoProj.thy src/HOL/Lex/Automata.thy src/HOL/Lex/Chopper.thy src/HOL/Lex/DA.thy src/HOL/Lex/MaxChop.thy src/HOL/Lex/MaxPrefix.thy src/HOL/Lex/NA.thy src/HOL/Lex/NAe.thy src/HOL/Lex/README.html src/HOL/Lex/ROOT.ML src/HOL/Lex/RegExp.thy src/HOL/Lex/RegExp2NA.thy src/HOL/Lex/RegExp2NAe.thy src/HOL/Lex/RegSet.thy src/HOL/Lex/RegSet_of_nat_DA.thy src/HOL/Lex/Scanner.thy

2004-03-31 streckem [Wed, 31 Mar 2004 10:51:50 +0200] rev 14500
new
doc-src/Exercises/0304/a1/generated/a1.tex doc-src/Exercises/0304/a1/generated/session.tex doc-src/Exercises/0304/a2/generated/a2.tex doc-src/Exercises/0304/a2/generated/session.tex doc-src/Exercises/0304/a3/generated/a3.tex doc-src/Exercises/0304/a3/generated/session.tex doc-src/Exercises/0304/a4/generated/a4.tex doc-src/Exercises/0304/a4/generated/session.tex doc-src/Exercises/0304/a5/generated/a5.tex doc-src/Exercises/0304/a5/generated/session.tex

2004-03-30 streckem [Tue, 30 Mar 2004 19:33:57 +0200] rev 14499
new
doc-src/Exercises/0304/IsaMakefile doc-src/Exercises/0304/Makefile doc-src/Exercises/0304/a1/ROOT.ML doc-src/Exercises/0304/a1/a1.thy doc-src/Exercises/0304/a2/ROOT.ML doc-src/Exercises/0304/a2/a2.thy doc-src/Exercises/0304/a3/ROOT.ML doc-src/Exercises/0304/a3/a3.thy doc-src/Exercises/0304/a4/ROOT.ML doc-src/Exercises/0304/a4/a4.thy doc-src/Exercises/0304/a5/ROOT.ML doc-src/Exercises/0304/a5/a5.thy