equal
deleted
inserted
replaced
102 if qa = q then exqu ((qC,x,T)::xs) Q else NONE |
102 if qa = q then exqu ((qC,x,T)::xs) Q else NONE |
103 | exqu xs P = extract xs P |
103 | exqu xs P = extract xs P |
104 in exqu end; |
104 in exqu end; |
105 |
105 |
106 fun prove_conv tac thy tu = |
106 fun prove_conv tac thy tu = |
107 Goal.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac)); |
107 Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu) |
|
108 (K (rtac iff_reflection 1 THEN tac)); |
108 |
109 |
109 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) |
110 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) |
110 |
111 |
111 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) |
112 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) |
112 Better: instantiate exI |
113 Better: instantiate exI |