src/HOL/Bali/Basis.thy

--- a/src/HOL/Bali/Basis.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/Basis.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -28,7 +28,9 @@
 change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
 *}
 declare if_weak_cong [cong del] option.weak_case_cong [cong del]
-declare length_Suc_conv [iff];
+declare length_Suc_conv [iff]
+
+declare not_None_eq [iff]
 
 (*###to be phased out *)
 ML {*