--- a/Nominal/Ex/TypeSchemes.thy	Sat Feb 05 07:39:00 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Mon Feb 07 15:59:37 2011 +0000
@@ -4,40 +4,6 @@
 
 section {*** Type Schemes ***}
 
-nominal_datatype 
-  A = Aa bool | Ab B
-and 
-  B = Ba bool | Bb A
-
-lemma
-  "(p \<bullet> (Sum_Type.Projl (f (Inl x)))) = Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> x)))"
-apply(perm_simp)
-apply(subst permute_fun_def)
-sorry
-
-nominal_primrec
-    even :: "nat \<Rightarrow> A"
-and odd  :: "nat \<Rightarrow> B"
-where
-  "even 0 = Aa True"
-| "even (Suc n) = Ab (odd n)"
-| "odd 0 = Ba False"
-| "odd (Suc n) = Bb (even n)"
-thm even_odd_graph.intros even_odd_sumC_def
-thm sum.cases Product_Type.split
-thm even_odd_graph_def 
-term Inr
-term Sum_Type.Projr
-term even_odd_sumC
-thm even_odd_sumC_def
-unfolding even_odd_sumC_def
-sorry
-
-ML {* the *}
-
-thm even.psimps odd.psimps
-
-
 
 atom_decl name