src/Pure/Isar/object_logic.ML
changeset 12829 c92128238f85
parent 12807 4f2983e39a59
child 13197 0567f4fd1415
     1.1 --- a/src/Pure/Isar/object_logic.ML	Mon Jan 21 15:29:06 2002 +0100
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Mon Jan 21 16:15:16 2002 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    val declare_rulify: theory attribute
     1.5    val atomize_term: Sign.sg -> term -> term
     1.6    val atomize_tac: int -> tactic
     1.7 +  val full_atomize_tac: int -> tactic
     1.8    val atomize_goal: int -> thm -> thm
     1.9    val rulify: thm -> thm
    1.10    val rulify_no_asm: thm -> thm
    1.11 @@ -135,6 +136,9 @@
    1.12      (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
    1.13    else all_tac st;
    1.14  
    1.15 +fun full_atomize_tac i st =
    1.16 +  rewrite_goal_tac (get_atomize (Thm.sign_of_thm st)) i st;
    1.17 +
    1.18  fun atomize_goal i st =
    1.19    (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');
    1.20