src/HOL/simpdata.ML
changeset 2054 bf3891343aa5
parent 2036 62ff902eeffc
child 2082 8659e3063a30
equal deleted inserted replaced
2053:6c0594bfa726 2054:bf3891343aa5
   118      "(P & False) = False", "(False & P) = False", "(P & P) = P",
   118      "(P & False) = False", "(False & P) = False", "(P & P) = P",
   119      "(P | True) = True", "(True | P) = True", 
   119      "(P | True) = True", "(True | P) = True", 
   120      "(P | False) = P", "(False | P) = P", "(P | P) = P",
   120      "(P | False) = P", "(False | P) = P", "(P | P) = P",
   121      "((~P) = (~Q)) = (P=Q)",
   121      "((~P) = (~Q)) = (P=Q)",
   122      "(!x.P) = P", "(? x.P) = P", "? x. x=t", 
   122      "(!x.P) = P", "(? x.P) = P", "? x. x=t", 
   123      "(? x. x=t & P(x)) = P(t)", "(! x. x=t --> P(x)) = P(t)" ];
   123      "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", 
       
   124      "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
   124 
   125 
   125 in
   126 in
   126 
   127 
   127 val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y"
   128 val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y"
   128   (fn [prem] => [rewtac prem, rtac refl 1]);
   129   (fn [prem] => [rewtac prem, rtac refl 1]);