# HG changeset patch
# User wenzelm
# Date 1142350178 -3600
# Node ID 9f8e56d1dbf6b051b4e8f15bc51f2c9c897b4121
# Parent  a3d3a4b75c71e76b95774e3da89c68009fbb7784
added is_elim (from Provers/classical.ML);

diff -r a3d3a4b75c71 -r 9f8e56d1dbf6 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue Mar 14 16:29:37 2006 +0100
+++ b/src/Pure/Isar/object_logic.ML	Tue Mar 14 16:29:38 2006 +0100
@@ -14,6 +14,7 @@
   val drop_judgment: theory -> term -> term
   val fixed_judgment: theory -> string -> term
   val ensure_propT: theory -> term -> term
+  val is_elim: thm -> bool
   val declare_atomize: attribute
   val declare_rulify: attribute
   val atomize_term: theory -> term -> term
@@ -115,6 +116,18 @@
   in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
 
 
+(* elimination rules *)
+
+fun is_elim rule =
+  let
+    val thy = Thm.theory_of_thm rule;
+    val concl = Thm.concl_of rule;
+  in
+    Term.is_Var (drop_judgment thy concl) andalso
+      exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
+  end;
+
+
 
 (** treatment of meta-level connectives **)