# HG changeset patch
# User paulson
# Date 877078850 -7200
# Node ID 96e28b16861c6972f8536fd09e805d74daa2baed
# Parent  4ed64ad7fb42aa7507a5e6d5c0029f69596ccf6b
New trivial rewrites

diff -r 4ed64ad7fb42 -r 96e28b16861c src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Oct 17 11:00:00 1997 +0200
+++ b/src/HOL/simpdata.ML	Fri Oct 17 11:00:50 1997 +0200
@@ -103,9 +103,11 @@
    "(P & True) = P", "(True & P) = P", 
    "(P & False) = False", "(False & P) = False",
    "(P & P) = P", "(P & (P & Q)) = (P & Q)",
+   "(P & ~P) = False",    "(~P & P) = False",
    "(P | True) = True", "(True | P) = True", 
    "(P | False) = P", "(False | P) = P",
    "(P | P) = P", "(P | (P | Q)) = (P | Q)",
+   "(P | ~P) = True",    "(~P | P) = True",
    "((~P) = (~Q)) = (P=Q)",
    "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", 
    "(? x. x=t & P(x)) = P(t)",
@@ -312,6 +314,10 @@
                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
                    (fn _ => [rtac expand_if 1]);
 
+
+
+(** Case splitting **)
+
 local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
 in
 fun split_tac splits = mktac (map mk_meta_eq splits)