src/HOL/MiniML/Maybe.ML
changeset 2031 03a843f0f447
parent 1757 f7a573c46611
child 2058 ff04984186e9
--- a/src/HOL/MiniML/Maybe.ML	Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/MiniML/Maybe.ML	Thu Sep 26 12:47:47 1996 +0200
@@ -21,8 +21,8 @@
 
 goal Maybe.thy
   "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
-by(simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
-by(fast_tac HOL_cs 1);
+by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (fast_tac HOL_cs 1);
 qed "bind_eq_Fail";
 
 Addsimps [bind_eq_Fail];