2006-06-12 wenzelm [Mon, 12 Jun 2006 21:19:00 +0200] rev 19861
tuned Seq/Envir/Unify interfaces;
src/HOL/TLA/Intensional.ML src/HOL/Tools/inductive_codegen.ML src/Provers/IsaPlanner/isand.ML src/Provers/IsaPlanner/zipper.ML src/Provers/eqsubst.ML src/Provers/induct_method.ML src/Pure/Isar/calculation.ML src/Pure/drule.ML src/Pure/envir.ML src/Pure/tctical.ML src/Pure/thm.ML

2006-06-12 wenzelm [Mon, 12 Jun 2006 21:18:10 +0200] rev 19860
fixed subst step;
src/HOL/ex/MergeSort.thy

2006-06-12 wenzelm [Mon, 12 Jun 2006 20:58:25 +0200] rev 19859
avoid accidental binding of ?Jmp;
src/HOL/Bali/DefiniteAssignmentCorrect.thy

2006-06-12 urbanc [Mon, 12 Jun 2006 20:32:33 +0200] rev 19858
added lemma fresh_unit to Nominal.thy
made the fresh_guess tactic to solve more goals
adapted Iteration.thy to use the new tactic
src/HOL/Nominal/Examples/Iteration.thy src/HOL/Nominal/Nominal.thy src/HOL/Nominal/nominal_permeq.ML

2006-06-12 berghofe [Mon, 12 Jun 2006 18:17:21 +0200] rev 19857
Added fresh_guess_tac.
src/HOL/Nominal/nominal_permeq.ML

2006-06-12 berghofe [Mon, 12 Jun 2006 18:15:45 +0200] rev 19856
Removed comments around declaration of fresh_guess method.
src/HOL/Nominal/Nominal.thy

2006-06-12 berghofe [Mon, 12 Jun 2006 17:16:03 +0200] rev 19855
Added "evaluation" method.
NEWS

2006-06-12 haftmann [Mon, 12 Jun 2006 15:58:12 +0200] rev 19854
updated keywords
etc/isar-keywords-HOL-Nominal.el etc/isar-keywords-ZF.el etc/isar-keywords.el

2006-06-12 wenzelm [Mon, 12 Jun 2006 11:59:25 +0200] rev 19853
made smlnj happy;
src/Provers/IsaPlanner/zipper.ML

2006-06-12 haftmann [Mon, 12 Jun 2006 09:14:41 +0200] rev 19852
fixed smlnj incompat.
src/Pure/Tools/invoke.ML