diff -r 817a34a54fb0 -r 946efd210837 src/HOL/MiniML/Maybe.ML --- a/src/HOL/MiniML/Maybe.ML Mon May 20 10:11:30 1996 +0200 +++ b/src/HOL/MiniML/Maybe.ML Mon May 20 18:41:55 1996 +0200 @@ -18,3 +18,7 @@ by (fast_tac (HOL_cs addss !simpset) 1); by (Asm_simp_tac 1); qed "expand_bind"; + +goal Maybe.thy "!!x. x = Ok y ==> x ~= Fail"; +by(Asm_simp_tac 1); +qed "eq_OkD";