Mercurial Mercurial > repos > isabelle / 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.
Simpset removes the de Morgan laws
authorpaulson
Thu, 10 Oct 1996 11:58:40 +0200
changeset 2087 6405a3bb490b
parent 2086 80ef03e39058
child 2088 e814e03bbbb2
Simpset removes the de Morgan laws
src/HOL/Subst/Subst.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Subst/Subst.ML	Thu Oct 10 11:13:48 1996 +0200
+++ b/src/HOL/Subst/Subst.ML	Thu Oct 10 11:58:40 1996 +0200
@@ -29,7 +29,8 @@
    val Var_subst = mk_thm "Var(x) <| al = assoc x (Var x) al";
 end;
 
-val subst_ss = raw_subst_ss addsimps subst_rews;
+val subst_ss = raw_subst_ss addsimps subst_rews 
+                            delsimps [de_Morgan_conj, de_Morgan_disj];
 
 (**** Substitutions ****)
isabelle