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 sg tu = |
106 fun prove_conv tac sg tu = |
107 let val meta_eq = cterm_of sg (Logic.mk_equals tu) |
107 Tactic.prove sg [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac)); |
108 in prove_goalw_cterm [] meta_eq (K [rtac iff_reflection 1, tac]) |
|
109 handle ERROR => |
|
110 error("The error(s) above occurred while trying to prove " ^ |
|
111 string_of_cterm meta_eq) |
|
112 end; |
|
113 |
108 |
114 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) |
109 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) |
115 |
110 |
116 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) |
111 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) |
117 Better: instantiate exI |
112 Better: instantiate exI |