2002-11-17 berghofe [Sun, 17 Nov 2002 23:43:53 +0100] rev 13719
Fixed small bug that caused some definitions to be "forgotten".
src/Pure/Proof/extraction.ML

2002-11-16 kleing [Sat, 16 Nov 2002 23:01:59 +0100] rev 13718
beautified "match"
src/HOL/MicroJava/BV/EffectMono.thy

2002-11-16 kleing [Sat, 16 Nov 2002 22:54:39 +0100] rev 13717
beautified "match"
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy src/HOL/MicroJava/BV/Effect.thy

2002-11-15 nipkow [Fri, 15 Nov 2002 18:02:25 +0100] rev 13716
added zdvd_iff_zmod_eq_0
src/HOL/Integ/IntDiv.thy

2002-11-13 berghofe [Wed, 13 Nov 2002 15:36:36 +0100] rev 13715
Improved function decompose.
src/Pure/Proof/reconstruct.ML

2002-11-13 berghofe [Wed, 13 Nov 2002 15:36:06 +0100] rev 13714
- exported functions etype_of and mk_typ
- new function realizes_of
src/Pure/Proof/extraction.ML

2002-11-13 berghofe [Wed, 13 Nov 2002 15:35:15 +0100] rev 13713
Fixed name clash problem in forall_elim_var.
src/Pure/pure_thy.ML

2002-11-13 berghofe [Wed, 13 Nov 2002 15:34:35 +0100] rev 13712
Added simple_prove_goal_cterm.
src/Pure/goals.ML

2002-11-13 berghofe [Wed, 13 Nov 2002 15:34:01 +0100] rev 13711
Removed (now unneeded) declarations of realizers for bar induction.
src/HOL/Extraction/Higman.thy

2002-11-13 berghofe [Wed, 13 Nov 2002 15:32:41 +0100] rev 13710
New package for constructing realizers for introduction and elimination
rules of inductive predicates.
src/HOL/Tools/inductive_realizer.ML