--- a/src/HOL/UNITY/Channel.ML Fri May 21 16:26:06 1999 +0200
+++ b/src/HOL/UNITY/Channel.ML Mon May 24 15:43:45 1999 +0200
@@ -26,15 +26,12 @@
Goal "F : (minSet -`` {Some x}) leadsTo (minSet -`` (Some``greaterThan x))";
by (rtac leadsTo_weaken 1);
-by (rtac ([UC2, UC1] MRS psp) 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
+by (res_inst_tac [("x1","x")] ([UC2, UC1] MRS psp) 1);
by Safe_tac;
by (auto_tac (claset() addDs [minSet_eq_SomeD],
- simpset() addsimps [le_def, linorder_neq_iff]));
+ simpset() addsimps [linorder_neq_iff]));
qed "minSet_greaterThan";
-
(*The induction*)
Goal "F : (UNIV-{{}}) leadsTo (minSet -`` (Some``atLeast y))";
by (rtac leadsTo_weaken_R 1);