# HG changeset patch
# User lcp
# Date 772455713 -7200
# Node ID 1577cbcd0936413eae85718f6668fbeab0b9dac1
# Parent  ad3f46c13f1e0682afdc51bcc5be18bbdad2306e
FOL/FOL.ML/excluded_middle_tac: new

diff -r ad3f46c13f1e -r 1577cbcd0936 src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Fri Jun 24 10:45:02 1994 +0200
+++ b/src/FOL/FOL.ML	Fri Jun 24 13:01:53 1994 +0200
@@ -12,6 +12,7 @@
   sig
   val disjCI : thm
   val excluded_middle : thm
+  val excluded_middle_tac : string -> int -> tactic
   val exCI : thm
   val ex_classical : thm
   val iffCE : thm
@@ -52,6 +53,9 @@
 val excluded_middle = prove_goal FOL.thy "~P | P"
  (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
 
+(*For disjunctive case analysis*)
+fun excluded_middle_tac sP =
+    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
 
 (*** Special elimination rules *)