equal
deleted
inserted
replaced
47 |
47 |
48 (** generic proof tools **) |
48 (** generic proof tools **) |
49 |
49 |
50 (* prove conversions *) |
50 (* prove conversions *) |
51 |
51 |
52 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
52 fun prove_conv expand_tac norm_tac sg ss tu = (* FIXME avoid standard *) |
53 |
53 mk_meta_eq (standard (Goal.prove sg [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq tu)) |
54 fun prove_conv expand_tac norm_tac sg ss tu = |
54 (K [expand_tac, norm_tac ss]))); |
55 mk_meta_eq (OldGoals.prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu)) |
|
56 (K [expand_tac, norm_tac ss])) |
|
57 handle ERROR => error ("The error(s) above occurred while trying to prove " ^ |
|
58 (string_of_cterm (cterm_of sg (mk_eqv tu)))); |
|
59 |
55 |
60 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s" |
56 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s" |
61 (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]); |
57 (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]); |
62 |
58 |
63 |
59 |