Mercurial Mercurial > repos > Old_HOL / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
used new field "simps" of Datatype
authornipkow
Tue, 22 Mar 1994 19:55:29 +0100
changeset 61 ab88297f1a56
parent 60 43e36c15a831
child 62 32a83e3ad5a4
used new field "simps" of Datatype
ex/PL.ML file | annotate | diff | comparison | revisions
ex/pl.ML file | annotate | diff | comparison | revisions 
--- 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);
--- 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);
Old_HOL