src/HOL/Bali/Evaln.thy
changeset 22218 30a8890d2967
parent 21765 89275a3ed7be
child 23350 50c5b0912a0c
--- a/src/HOL/Bali/Evaln.thy	Wed Jan 31 14:03:31 2007 +0100
+++ b/src/HOL/Bali/Evaln.thy	Wed Jan 31 16:05:10 2007 +0100
@@ -191,7 +191,7 @@
           \<Longrightarrow>
 		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
 monos
-  if_def2
+  if_bool_eq_conj
 
 
 declare split_if     [split del] split_if_asm     [split del]