# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272964329 -7200
# Node ID 94e24da9ae7542649c8d341c31a24b3d26be63f9
# Parent  39df91a90f87177d2bcf0ff4b5a25ff628a49115
Move TypeSchemes to NewParser

diff -r 39df91a90f87 -r 94e24da9ae75 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Tue May 04 11:08:30 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Tue May 04 11:12:09 2010 +0200
@@ -1,18 +1,16 @@
 theory TypeSchemes
-imports "../Parser"
+imports "../NewParser"
 begin
 
 section {*** Type Schemes ***}
 
 atom_decl name
 
-ML {* val _ = alpha_type := AlphaRes *}
-
 nominal_datatype ty =
   Var "name"
 | Fun "ty" "ty"
 and tys =
-  All xs::"name fset" ty::"ty" bind xs in ty
+  All xs::"name fset" ty::"ty" bind_res xs in ty
 
 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
 
@@ -125,21 +123,21 @@
   apply(simp add: ty_tys.eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alphas)
-  apply(simp add: fresh_star_def fresh_zero_perm)
+  apply(simp add: fresh_star_def fresh_zero_perm supp_at_base)
   done
 
 lemma
   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
   apply(simp add: ty_tys.eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alphas fresh_star_def eqvts)
+  apply(simp add: alphas fresh_star_def eqvts supp_at_base)
   done
 
 lemma
   shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
   apply(simp add: ty_tys.eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff)
+  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
 done
 
 lemma
@@ -148,7 +146,7 @@
   using a
   apply(simp add: ty_tys.eq_iff)
   apply(clarify)
-  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff)
+  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
   apply auto
   done