diff -r a6f3e1b08494 -r b6873d123f9b Tutorial/Tutorial6.thy
--- a/Tutorial/Tutorial6.thy	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-theory Tutorial6
-imports "../Nominal/Nominal2"
-begin
-
-
-section {* Type Schemes *}
-
-text {*
-  Nominal2 can deal also with more complicated binding
-  structures; for example the finite set of binders found
-  in type schemes.
-*}
-
-atom_decl name
-
-nominal_datatype ty =
-  Var "name"
-| Fun "ty" "ty" (infixr "\<rightarrow>" 100)
-and tys =
-  All as::"name fset" ty::"ty" binds (set+) as in ty ("All _. _" [100, 100] 100)
-
-
-text {* Some alpha-equivalences *}
-
-lemma
-  shows "All {|a, b|}. (Var a) \<rightarrow> (Var b) = All {|b, a|}. (Var a) \<rightarrow> (Var b)"
-  unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def
-  by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def intro: permute_zero)
-  
-lemma
-  shows "All {|a, b|}. (Var a) \<rightarrow> (Var b) = All {|a, b|}. (Var b) \<rightarrow> (Var a)"
-  unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def
-  by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def swap_atom)
-     (metis permute_flip_at)
-  
-lemma
-  shows "All {|a, b, c|}. (Var a) \<rightarrow> (Var b) = All {|a, b|}. (Var a) \<rightarrow> (Var b)"
-  unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def
-  by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def intro: permute_zero)
-  
-lemma
-  assumes a: "a \<noteq> b"
-  shows "All {|a, b|}. (Var a) \<rightarrow> (Var b) \<noteq> All {|c|}. (Var c) \<rightarrow> (Var c)"
-  using a
-  unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def
-  by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def)
-
-
-end
\ No newline at end of file