src/HOL/Option.ML
changeset 4752 1c334bd00038
parent 4477 b3e5857d8d99
child 4800 97c3a45d092b
--- a/src/HOL/Option.ML	Tue Mar 24 15:49:32 1998 +0100
+++ b/src/HOL/Option.ML	Tue Mar 24 15:51:37 1998 +0100
@@ -57,3 +57,16 @@
 	"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
 	optionE_tac "x" 1,
 	 Auto_tac]);
+
+section "o2s";
+
+val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
+ (K [	optionE_tac "xo" 1,
+	 Auto_tac]);
+AddSDs [elem_o2s RS iffD1];
+Addsimps [elem_o2s];
+
+val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)"
+ (K [	optionE_tac "xo" 1,
+	 Auto_tac]);
+Addsimps [o2s_empty_eq];