equal
deleted
inserted
replaced
186 fun dest_cprop ct = |
186 fun dest_cprop ct = |
187 (case Thm.term_of ct of |
187 (case Thm.term_of ct of |
188 @{const Trueprop} $ _ => Thm.dest_arg ct |
188 @{const Trueprop} $ _ => Thm.dest_arg ct |
189 | _ => raise CTERM ("not a property", [ct])) |
189 | _ => raise CTERM ("not a property", [ct])) |
190 |
190 |
191 val equals = mk_const_pat @{theory} @{const_name "=="} destT1 |
191 val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1 |
192 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu |
192 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu |
193 |
193 |
194 val dest_prop = (fn @{const Trueprop} $ t => t | t => t) |
194 val dest_prop = (fn @{const Trueprop} $ t => t | t => t) |
195 fun term_of ct = dest_prop (Thm.term_of ct) |
195 fun term_of ct = dest_prop (Thm.term_of ct) |
196 fun prop_of thm = dest_prop (Thm.prop_of thm) |
196 fun prop_of thm = dest_prop (Thm.prop_of thm) |