equal
deleted
inserted
replaced
96 fun Rel_conv ct = |
96 fun Rel_conv ct = |
97 let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct) |
97 let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct) |
98 val (cU, _) = dest_funcT cT' |
98 val (cU, _) = dest_funcT cT' |
99 in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end |
99 in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end |
100 |
100 |
101 fun Trueprop_conv cv ct = |
|
102 (case Thm.term_of ct of |
|
103 Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct |
|
104 | _ => raise CTERM ("Trueprop_conv", [ct])) |
|
105 |
|
106 (* Conversion to preprocess a transfer rule *) |
101 (* Conversion to preprocess a transfer rule *) |
107 fun prep_conv ct = ( |
102 fun prep_conv ct = ( |
108 Conv.implies_conv Conv.all_conv prep_conv |
103 Conv.implies_conv Conv.all_conv prep_conv |
109 else_conv |
104 else_conv |
110 Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) |
105 HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) |
111 else_conv |
106 else_conv |
112 Conv.all_conv) ct |
107 Conv.all_conv) ct |
113 |
108 |
114 (** Replacing explicit equalities with is_equality premises **) |
109 (** Replacing explicit equalities with is_equality premises **) |
115 |
110 |