# HG changeset patch
# User paulson
# Date 927553425 -7200
# Node ID 716d2d253a3c03723f037a905007debfaf354db1
# Parent  1471f2bd74a06f3840628453bd27929bca94c19f
updated for stronger version of psp

diff -r 1471f2bd74a0 -r 716d2d253a3c src/HOL/UNITY/Channel.ML
--- 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);