src/HOL/ex/MT.ML

--- a/src/HOL/ex/MT.ML	Tue Oct 10 10:34:42 2006 +0200
+++ b/src/HOL/ex/MT.ML	Tue Oct 10 10:34:43 2006 +0200
@@ -601,6 +601,9 @@
 (* The pointwise extension of hasty to environments             *)
 (* ############################################################ *)
 
+fun excluded_middle_tac sP =
+  res_inst_tac [("Q", sP)] (excluded_middle RS HOL.disjE);
+
 Goal "[| ve hastyenv te; v hasty t |] ==> \
 \        ve + {ev |-> v} hastyenv te + {ev |=> t}";
 by (rewtac hasty_env_def);