--- a/src/HOL/MiniML/Maybe.ML Mon Mar 01 13:51:21 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-(* Title: HOL/MiniML/Maybe.ML
- ID: $Id$
- Author: Wolfgang Naraschewski and Tobias Nipkow
- Copyright 1996 TU Muenchen
-*)
-
-(* constructor laws for option_bind *)
-Goalw [option_bind_def] "option_bind (Some s) f = (f s)";
-by (Simp_tac 1);
-qed "option_bind_Some";
-
-Goalw [option_bind_def] "option_bind None f = None";
-by (Simp_tac 1);
-qed "option_bind_None";
-
-Addsimps [option_bind_Some,option_bind_None];
-
-(* expansion of option_bind *)
-Goalw [option_bind_def] "P(option_bind res f) = \
-\ ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
-by (rtac option.split 1);
-qed "split_option_bind";
-
-Goal
- "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
-by (simp_tac (simpset() addsplits [split_option_bind]) 1);
-qed "option_bind_eq_None";
-
-Addsimps [option_bind_eq_None];
-
-(* auxiliary lemma *)
-Goal "(y = Some x) = (Some x = y)";
-by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-qed "rotate_Some";