# HG changeset patch
# User nipkow
# Date 797496058 -7200
# Node ID b860420000350983ad21c0d37c3fbe9b805d285b
# Parent  f5f36bdc80033a491dfb8252574a0f16aa6e0948
ROOT.ML: installed new hyp_subst_tac

Nat.ML: Changed proof of lessE for new hyp_subst_tac

diff -r f5f36bdc8003 -r b86042000035 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Mon Apr 10 08:13:13 1995 +0200
+++ b/src/HOL/Nat.ML	Mon Apr 10 08:40:58 1995 +0200
@@ -240,8 +240,9 @@
     "[| i<k;  k=Suc(i) ==> P;  !!j. [| i<j;  k=Suc(j) |] ==> P \
 \    |] ==> P";
 by (rtac (major RS tranclE) 1);
-by (fast_tac (HOL_cs addSEs (prems@[pred_natE, Pair_inject])) 1);
-by (fast_tac (HOL_cs addSEs (prems@[pred_natE, Pair_inject])) 1);
+by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE'
+		  eresolve_tac (prems@[pred_natE, Pair_inject])));
+by (rtac refl 1);
 qed "lessE";
 
 goal Nat.thy "~ n<0";
diff -r f5f36bdc8003 -r b86042000035 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Mon Apr 10 08:13:13 1995 +0200
+++ b/src/HOL/ROOT.ML	Mon Apr 10 08:40:58 1995 +0200
@@ -18,17 +18,19 @@
 use "thy_syntax.ML";
 
 use_thy "HOL";
+use "../Provers/simplifier.ML";
+use "../Provers/splitter.ML";
 use "../Provers/hypsubst.ML";
 use "../Provers/classical.ML";
-use "../Provers/simplifier.ML";
-use "../Provers/splitter.ML";
 
 (** Applying HypsubstFun to generate hyp_subst_tac **)
 
 structure Hypsubst_Data =
   struct
+  structure Simplifier = Simplifier
   (*Take apart an equality judgement; otherwise raise Match!*)
   fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
+  val eq_reflection = eq_reflection
   val imp_intr = impI
   val rev_mp = rev_mp
   val subst = subst