# HG changeset patch
# User oheimb
# Date 980877444 -3600
# Node ID ee0838d89debc58048e45bb6409c35631279cedd
# Parent  e33dfe9bde39849b1d3ab63f86920403782e7bb9
added if_def2

diff -r e33dfe9bde39 -r ee0838d89deb src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Jan 30 18:53:46 2001 +0100
+++ b/src/HOL/Inductive.thy	Tue Jan 30 18:57:24 2001 +0100
@@ -75,7 +75,7 @@
 setup PrimrecPackage.setup
 
 theorems basic_monos [mono] =
-  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
+  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
   Collect_mono in_mono vimage_mono
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
   not_all not_ex
diff -r e33dfe9bde39 -r ee0838d89deb src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Jan 30 18:53:46 2001 +0100
+++ b/src/HOL/simpdata.ML	Tue Jan 30 18:57:24 2001 +0100
@@ -233,6 +233,8 @@
 
 bind_thms ("if_splits", [split_if, split_if_asm]);
 
+bind_thm ("if_def2", read_instantiate [("P","\\<lambda>x. x")] split_if);
+
 Goal "(if c then x else x) = x";
 by (stac split_if 1);
 by (Blast_tac 1);