--- a/ex/PL.ML Sat Aug 13 16:33:53 1994 +0200
+++ b/ex/PL.ML Sat Aug 13 16:34:30 1994 +0200
@@ -135,7 +135,9 @@
(** The function eval **)
-val pl_ss = set_ss addsimps [pl_rec_var,pl_rec_false,pl_rec_imp] @ PL.pl.simps;
+val pl_ss = set_ss addsimps
+ (PL.pl.simps @ [eval2_false, eval2_var, eval2_imp]
+ @ [hyps_false, hyps_var, hyps_imp]);
goalw PL.thy [eval_def] "tt[false] = False";
by (simp_tac pl_ss 1);
@@ -151,22 +153,6 @@
val pl_ss = pl_ss addsimps [eval_false, eval_var, eval_imp];
-(** The function hyps **)
-
-goalw PL.thy [hyps_def] "hyps(false,tt) = {}";
-by (simp_tac pl_ss 1);
-val hyps_false = result();
-
-goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, #v->false)}";
-by (simp_tac pl_ss 1);
-val hyps_var = result();
-
-goalw PL.thy [hyps_def] "hyps(p->q,tt) = hyps(p,tt) Un hyps(q,tt)";
-by (simp_tac pl_ss 1);
-val hyps_imp = result();
-
-val pl_ss = pl_ss addsimps [hyps_false, hyps_var, hyps_imp];
-
val ball_eq = prove_goalw Set.thy [Ball_def] "(!x:A.P(x)) = (!x.x:A --> P(x))"
(fn _ => [rtac refl 1]);