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]); |