# HG changeset patch
# User urbanc
# Date 1133775210 -3600
# Node ID b9d0bd76286c091c020f7c8d940b58a0f60189af
# Parent  6bab9cef50cf78cb7e9423b4407f18388ef04e57
tuned

diff -r 6bab9cef50cf -r b9d0bd76286c src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Mon Dec 05 10:32:37 2005 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Mon Dec 05 10:33:30 2005 +0100
@@ -15,29 +15,15 @@
                      | App "lam" "lam"
                      | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
-datatype ty =
-    TVar "string"
+nominal_datatype ty =
+    TVar "nat"
   | TArr "ty" "ty" (infix "\<rightarrow>" 200)
 
-primrec
- "pi\<bullet>(TVar s) = TVar s"
- "pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)"
-
 lemma perm_ty[simp]:
   fixes pi ::"name prm"
   and   \<tau>  ::"ty"
   shows "pi\<bullet>\<tau> = \<tau>"
-  by (cases \<tau>, simp_all)
-
-instance ty :: pt_name
-apply(intro_classes)   
-apply(simp_all)
-done
-
-instance ty :: fs_name
-apply(intro_classes)
-apply(simp add: supp_def)
-done
+by (induct \<tau> rule: ty.induct_weak, simp_all add: perm_nat_def)  
 
 (* valid contexts *)
 consts