changeset 61 | ab88297f1a56 |
parent 56 | 385d51d74f71 |
child 66 | 14b9286ed036 |
--- a/ex/PL.ML Tue Mar 22 19:54:55 1994 +0100 +++ b/ex/PL.ML Tue Mar 22 19:55:29 1994 +0100 @@ -135,8 +135,7 @@ (** The function eval **) -val pl_ss = set_ss addsimps [pl_rec_var,pl_rec_false,pl_rec_imp] - @ PL0.inject @ PL0.ineq; +val pl_ss = set_ss addsimps [pl_rec_var,pl_rec_false,pl_rec_imp] @ PL0.simps; goalw PL.thy [eval_def] "tt[false] = False"; by (simp_tac pl_ss 1);