--- a/Nominal/Ex/Let.thy	Sat Feb 05 07:39:00 2011 +0900
+++ b/Nominal/Ex/Let.thy	Mon Feb 07 15:59:37 2011 +0000
@@ -100,6 +100,7 @@
 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (substa s t as) (subst s t b)"
 | "substa s t ANil = ANil"
 | "substa s t (ACons v t' as) = ACons v (subst v t t') as"
+oops
 
 (*apply (subgoal_tac "\<forall>l. \<exists>!r. subst_substa_graph l r")
 defer
@@ -113,6 +114,7 @@
 apply rule
 apply (rule subst_substa_graph.intros)*)
 
+(*
 defer
 apply (case_tac x)
 apply (case_tac a)
@@ -163,7 +165,7 @@
          (Acons s (subst a t t') a2)
 
 ACons v (subst v t t') as"
-
+*)
 end
 
 

--- 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