equal
deleted
inserted
replaced
111 if qa = q then exqu ((qC,x,T)::xs) Q else NONE |
111 if qa = q then exqu ((qC,x,T)::xs) Q else NONE |
112 | exqu xs P = extract (null xs) xs P |
112 | exqu xs P = extract (null xs) xs P |
113 in exqu [] end; |
113 in exqu [] end; |
114 |
114 |
115 fun prove_conv tac thy tu = |
115 fun prove_conv tac thy tu = |
116 Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu) |
116 Goal.prove (ProofContext.init_global thy) [] [] (Logic.mk_equals tu) |
117 (K (rtac iff_reflection 1 THEN tac)); |
117 (K (rtac iff_reflection 1 THEN tac)); |
118 |
118 |
119 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) |
119 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) |
120 |
120 |
121 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) |
121 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) |