equal
deleted
inserted
replaced
145 Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct |
145 Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct |
146 | _ => Conv.all_conv ct |
146 | _ => Conv.all_conv ct |
147 |
147 |
148 fun Trueprop_conv cv ct = |
148 fun Trueprop_conv cv ct = |
149 case Thm.term_of ct of |
149 case Thm.term_of ct of |
150 Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct |
150 Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct |
151 | _ => raise Fail "Trueprop_conv" |
151 | _ => raise Fail "Trueprop_conv" |
152 |
152 |
153 fun preprocess_intro thy rule = |
153 fun preprocess_intro thy rule = |
154 Conv.fconv_rule |
154 Conv.fconv_rule |
155 (imp_prems_conv |
155 (imp_prems_conv |