src/HOL/simpdata.ML
changeset 3913 96e28b16861c
parent 3904 c0d56e4c823e
child 3919 c036caebfc75
     1.1 --- a/src/HOL/simpdata.ML	Fri Oct 17 11:00:00 1997 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Oct 17 11:00:50 1997 +0200
     1.3 @@ -103,9 +103,11 @@
     1.4     "(P & True) = P", "(True & P) = P", 
     1.5     "(P & False) = False", "(False & P) = False",
     1.6     "(P & P) = P", "(P & (P & Q)) = (P & Q)",
     1.7 +   "(P & ~P) = False",    "(~P & P) = False",
     1.8     "(P | True) = True", "(True | P) = True", 
     1.9     "(P | False) = P", "(False | P) = P",
    1.10     "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    1.11 +   "(P | ~P) = True",    "(~P | P) = True",
    1.12     "((~P) = (~Q)) = (P=Q)",
    1.13     "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", 
    1.14     "(? x. x=t & P(x)) = P(t)",
    1.15 @@ -312,6 +314,10 @@
    1.16                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    1.17                     (fn _ => [rtac expand_if 1]);
    1.18  
    1.19 +
    1.20 +
    1.21 +(** Case splitting **)
    1.22 +
    1.23  local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
    1.24  in
    1.25  fun split_tac splits = mktac (map mk_meta_eq splits)