# HG changeset patch
# User wenzelm
# Date 1298306603 -3600
# Node ID c3aa3c87ef218bc3023926d9498ec1d11ab7a2e5
# Parent  0c6093d596d636d078810a2a0602a27bf4a57689
modernized specifications;

diff -r 0c6093d596d6 -r c3aa3c87ef21 src/HOL/Nominal/Examples/CK_Machine.thy
--- a/src/HOL/Nominal/Examples/CK_Machine.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Mon Feb 21 17:43:23 2011 +0100
@@ -380,7 +380,7 @@
 
 text {* Typing Contexts *}
 
-types tctx = "(name\<times>ty) list"
+type_synonym tctx = "(name\<times>ty) list"
 
 text {* Sub-Typing Contexts *}
 
diff -r 0c6093d596d6 -r c3aa3c87ef21 src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy	Mon Feb 21 17:43:23 2011 +0100
@@ -2912,9 +2912,8 @@
 
 text {* typing contexts *}
 
-types 
-  ctxtn = "(name\<times>ty) list"
-  ctxtc = "(coname\<times>ty) list"
+type_synonym ctxtn = "(name\<times>ty) list"
+type_synonym ctxtc = "(coname\<times>ty) list"
 
 inductive
   validc :: "ctxtc \<Rightarrow> bool"
diff -r 0c6093d596d6 -r c3aa3c87ef21 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/Crary.thy	Mon Feb 21 17:43:23 2011 +0100
@@ -25,8 +25,8 @@
   | App "trm" "trm" ("App _ _" [110,110] 100)
   | Const "nat"
 
-types Ctxt  = "(name\<times>ty) list"
-types Subst = "(name\<times>trm) list" 
+type_synonym Ctxt  = "(name\<times>ty) list"
+type_synonym Subst = "(name\<times>trm) list" 
 
 
 lemma perm_ty[simp]: 
diff -r 0c6093d596d6 -r c3aa3c87ef21 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Mon Feb 21 17:43:23 2011 +0100
@@ -84,7 +84,7 @@
     VarB vrs ty 
   | TVarB tyvrs ty
 
-types env = "binding list"
+type_synonym env = "binding list"
 
 text {* Typing contexts are represented as lists that ``grow" on the left; we
   thereby deviating from the convention in the POPLmark-paper. The lists contain
diff -r 0c6093d596d6 -r c3aa3c87ef21 src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Mon Feb 21 17:43:23 2011 +0100
@@ -81,7 +81,7 @@
 
 text {* valid contexts *}
 
-types cxt = "(name\<times>ty) list"
+type_synonym cxt = "(name\<times>ty) list"
 
 inductive
   valid :: "cxt \<Rightarrow> bool"
diff -r 0c6093d596d6 -r c3aa3c87ef21 src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Mon Feb 21 17:43:23 2011 +0100
@@ -138,7 +138,7 @@
 lemma pat_type_perm_eq: "pat_type ((pi :: name prm) \<bullet> p) = pat_type p"
   by (induct p) (simp_all add: perm_type)
 
-types ctx = "(name \<times> ty) list"
+type_synonym ctx = "(name \<times> ty) list"
 
 inductive
   ptyping :: "pat \<Rightarrow> ty \<Rightarrow> ctx \<Rightarrow> bool"  ("\<turnstile> _ : _ \<Rightarrow> _" [60, 60, 60] 60)
diff -r 0c6093d596d6 -r c3aa3c87ef21 src/HOL/Nominal/Examples/Type_Preservation.thy
--- a/src/HOL/Nominal/Examples/Type_Preservation.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/Type_Preservation.thy	Mon Feb 21 17:43:23 2011 +0100
@@ -58,7 +58,7 @@
 
 text {* Typing Contexts *}
 
-types ctx = "(name\<times>ty) list"
+type_synonym ctx = "(name\<times>ty) list"
 
 abbreviation
   "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<subseteq> _") 
diff -r 0c6093d596d6 -r c3aa3c87ef21 src/HOL/Nominal/Examples/W.thy
--- a/src/HOL/Nominal/Examples/W.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/W.thy	Mon Feb 21 17:43:23 2011 +0100
@@ -53,7 +53,7 @@
 where
  "Let x be t1 in t2 \<equiv> trm.Let x t2 t1"
 
-types 
+type_synonym 
   Ctxt  = "(var\<times>tyS) list" 
 
 text {* free type variables *}
@@ -173,7 +173,7 @@
   
 text {* Substitution *}
 
-types Subst = "(tvar\<times>ty) list"
+type_synonym Subst = "(tvar\<times>ty) list"
 
 consts
   psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)
diff -r 0c6093d596d6 -r c3aa3c87ef21 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Mon Feb 21 17:43:23 2011 +0100
@@ -15,7 +15,7 @@
 section {* Permutations *}
 (*======================*)
 
-types 
+type_synonym 
   'x prm = "('x \<times> 'x) list"
 
 (* polymorphic constants for permutation and swapping *)