| changeset 1751 | 946efd210837 |
| parent 1300 | c7a8f374339b |
| child 1757 | f7a573c46611 |
--- 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";