diff -r 52771c21d9ca -r 14b9286ed036 ex/PL.ML
--- a/ex/PL.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/ex/PL.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -174,8 +174,8 @@
 val [major] = goalw PL.thy [sat_def] "H |- p ==> H |= p";
 by (rtac (major RS conseq_induct) 1);
 by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5);
-by (ALLGOALS (asm_simp_tac(pl_ss addsimps
-                [ball_eq,not_def RS fun_cong RS sym])));
+by (ALLGOALS (asm_simp_tac(pl_ss addsimps [ball_eq])));
+by(fast_tac HOL_cs 1);
 val soundness = result();
 
 (** Structural induction on pl
@@ -261,8 +261,7 @@
 goal PL.thy "hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{(#v)->false})";
 by (PL0.induct_tac "p" 1);
 by (simp_tac pl_ss 1);
-by (simp_tac (pl_ss addsimps [insert_subset]
-                    setloop (split_tac [expand_if])) 1);
+by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
 by (simp_tac pl_ss 1);
 by (fast_tac set_cs 1);
 val hyps_insert = result();