src/Pure/Isar/object_logic.ML
changeset 14743 81001d6cb8c0
parent 14226 7afe0e5bcc83
child 14854 61bdf2ae4dc5
     1.1 --- a/src/Pure/Isar/object_logic.ML	Thu May 13 16:02:29 2004 +0200
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Fri May 14 16:48:37 2004 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val declare_atomize: theory attribute
     1.5    val declare_rulify: theory attribute
     1.6    val atomize_term: Sign.sg -> term -> term
     1.7 +  val atomize_thm: thm -> thm
     1.8    val atomize_rule: Sign.sg -> cterm -> thm
     1.9    val atomize_tac: int -> tactic
    1.10    val full_atomize_tac: int -> tactic
    1.11 @@ -153,6 +154,10 @@
    1.12  
    1.13  fun atomize_rule sg = Tactic.rewrite true (get_atomize sg);
    1.14  
    1.15 +(*Convert a natural-deduction rule into a formula (probably in FOL)*)
    1.16 +fun atomize_thm th =
    1.17 +  rewrite_rule  (get_atomize (Thm.sign_of_thm th)) th;
    1.18 +
    1.19  fun atomize_tac i st =
    1.20    if Logic.has_meta_prems (Thm.prop_of st) i then
    1.21      (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st