diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/TypeRel.ML
--- a/src/HOL/MicroJava/J/TypeRel.ML	Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.ML	Mon Jan 03 14:07:08 2000 +0100
@@ -14,12 +14,6 @@
 \ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})"
  (K [Auto_tac]);
 
-context Option.thy;
-Goal "{y. x = Some y} \\<subseteq> {the x}";
-by Auto_tac;
-val some_subset_the = result();
-context thy;
-
 Goal "finite (subcls1 G)";
 by(stac subcls1_def2 1);
 by( rtac finite_SigmaI 1);
@@ -38,21 +32,11 @@
 	auto_tac (claset() addDs lemmata, simpset())]);
 
 
-(*#### patch for Isabelle98-1*)
-val major::prems = goal Trancl.thy
- "\\<lbrakk> (x,y) \\<in> r^+; \
-\    \\<And>x y. (x,y) \\<in> r \\<Longrightarrow> P x y; \
-\    \\<And>x y z. \\<lbrakk> (x,y) \\<in> r^+; P x y; (y,z) \\<in> r^+; P y z \\<rbrakk> \\<Longrightarrow> P x z \
-\ \\<rbrakk> \\<Longrightarrow> P x y";
-by(blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
-qed "trancl_trans_induct";
-
-Goalw [is_class_def] "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> is_class G C";
+Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ \\<Longrightarrow> is_class G C";
 by(etac trancl_trans_induct 1);
 by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
 qed "subcls_is_class";
 
-
 (* A particular thm about wf;
    looks like it is an odd instance of something more general
 *)
@@ -66,7 +50,7 @@
 by (Fast_tac 1);
 by(rewrite_goals_tac [wf_def]);
 by(Blast_tac 1);
-val wf_rel_lemma = result();
+qed "wf_rel_lemma";
 
 
 (* Proving the termination conditions *)
@@ -74,7 +58,7 @@
 goalw thy [subcls1_rel_def] "wf subcls1_rel";
 by(rtac (wf_rel_lemma RS wf_subset) 1);
 by(Force_tac 1);
-val wf_subcls1_rel = result();
+qed "wf_subcls1_rel";
 
 val method_TC = prove_goalw_cterm [subcls1_rel_def]
  (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (method.tcs)))))
@@ -111,21 +95,19 @@
 val widen_Class_NullT = prove_typerel "G\\<turnstile>Class C\\<preceq>RefT NullT \\<Longrightarrow> R" 
  [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT NullT \\<longrightarrow> R"];
 
-val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>Class cm \\<Longrightarrow> C=cm |  G\\<turnstile>C\\<prec>C cm"
-[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> C=cm |  G\\<turnstile>C\\<prec>C cm"];
+val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>Class cm \\<Longrightarrow> G\\<turnstile>C\\<prec>C cm"
+[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> G\\<turnstile>C\\<prec>C cm"];
 
-Goal "\\<lbrakk>G\\<turnstile>S\\<preceq>U; \\<forall>C. is_class G C \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object;\
-\\\<forall>C. G\\<turnstile>Object\\<prec>C C \\<longrightarrow> False \\<rbrakk> \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
+Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
 by( etac widen.induct 1);
 by   Safe_tac;
 by(  ALLGOALS (forward_tac [widen_Class, widen_RefT]));
 by  Safe_tac;
 by(  rtac widen.null 2);
-by( forward_tac [widen_Class_Class] 1);
-by Safe_tac;
-by(  ALLGOALS(EVERY'[etac thin_rl,etac thin_rl,
-	fast_tac (claset() addIs [widen.subcls,trancl_trans])]));
-qed_spec_mp "widen_trans_lemma";
+by(dtac widen_Class_Class 1);
+by(rtac widen.subcls 1);
+by(eatac rtrancl_trans 1 1);
+qed_spec_mp "widen_trans";
 
 
 val prove_cast_lemma = prove_typerel_lemma [] cast.elim;