--- a/src/Pure/Isar/object_logic.ML Thu May 13 16:02:29 2004 +0200
+++ b/src/Pure/Isar/object_logic.ML Fri May 14 16:48:37 2004 +0200
@@ -18,6 +18,7 @@
val declare_atomize: theory attribute
val declare_rulify: theory attribute
val atomize_term: Sign.sg -> term -> term
+ val atomize_thm: thm -> thm
val atomize_rule: Sign.sg -> cterm -> thm
val atomize_tac: int -> tactic
val full_atomize_tac: int -> tactic
@@ -153,6 +154,10 @@
fun atomize_rule sg = Tactic.rewrite true (get_atomize sg);
+(*Convert a natural-deduction rule into a formula (probably in FOL)*)
+fun atomize_thm th =
+ rewrite_rule (get_atomize (Thm.sign_of_thm th)) th;
+
fun atomize_tac i st =
if Logic.has_meta_prems (Thm.prop_of st) i then
(rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st