--- 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();