# HG changeset patch
# User paulson
# Date 844941520 -7200
# Node ID 6405a3bb490b55e15e8f65f0add55d1346cc1cbf
# Parent  80ef03e390581d9b9c7d620db149563ea641bf86
Simpset removes the de Morgan laws

diff -r 80ef03e39058 -r 6405a3bb490b src/HOL/Subst/Subst.ML
--- 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 ****)