--- a/LamEx.thy	Fri Dec 04 17:50:02 2009 +0100
+++ b/LamEx.thy	Fri Dec 04 17:57:03 2009 +0100
@@ -250,50 +250,3 @@
   apply(simp add: var_supp)
   done
 
-
-
-
-
-
-
-
-
-
-
-
-(* Construction Site code *)
-
-
-fun
-  option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
-where
-  "option_map f (nSome x) = nSome (f x)"
-| "option_map f nNone = nNone"
-
-fun
-  option_rel
-where
-  "option_rel r (nSome x) (nSome y) = r x y"
-| "option_rel r _ _ = False"
-
-declare [[map noption = (option_map, option_rel)]]
-
-lemma "option_map id = id"
-sorry
-
-lemma option_Quotient:
-  assumes q: "Quotient R Abs Rep"
-  shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)"
-  apply (unfold Quotient_def)
-  apply (auto)
-  using q
-  apply (unfold Quotient_def)
-  apply (case_tac "a :: 'b noption")
-  apply (simp)
-  apply (simp)
-  apply (case_tac "a :: 'b noption")
-  apply (simp only: option_map.simps)
-  apply (subst option_rel.simps)
-  (* Simp starts hanging so don't know how to continue *)
-  sorry
-