equal
deleted
inserted
replaced
20 |
20 |
21 (* export_defs *) |
21 (* export_defs *) |
22 |
22 |
23 local |
23 local |
24 |
24 |
25 val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal)); |
25 val refl_tac = Tactic.rtac (Drule.reflexive_thm RS Drule.triv_goal); |
26 |
26 |
27 fun dest_lhs cprop = |
27 fun dest_lhs cprop = |
28 let val x = #1 (Logic.dest_equals (Logic.dest_goal (Thm.term_of cprop))) |
28 let val x = #1 (Logic.dest_equals (Logic.dest_goal (Thm.term_of cprop))) |
29 in Term.dest_Free x; Thm.cterm_of (Thm.sign_of_cterm cprop) x end |
29 in Term.dest_Free x; Thm.cterm_of (Thm.sign_of_cterm cprop) x end |
30 handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^ |
30 handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^ |