cleanup type translations;
authorwenzelm
Wed Mar 03 00:33:02 2010 +0100 (2010-03-03)
changeset 354318758fe1fc9f8
parent 35430 df2862dc23a8
child 35432 b8863ee98f56
cleanup type translations;
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Name.thy
src/HOL/Bali/State.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/Term.thy
src/HOL/Bali/Type.thy
src/HOL/Bali/Value.thy
src/HOL/Bali/WellType.thy
src/HOL/IMPP/Hoare.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/MicroJava/J/Decl.thy
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/Decl.thy
src/HOL/NanoJava/State.thy
src/HOLCF/One.thy
src/HOLCF/Representable.thy
src/HOLCF/Tr.thy
     1.1 --- a/src/HOL/Bali/AxSem.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -58,10 +58,9 @@
     1.4    "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> CONST the_In3"
     1.5  
     1.6    --{* relation on result values, state and auxiliary variables *}
     1.7 -types 'a assn   =        "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
     1.8 +types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
     1.9  translations
    1.10 -      "res"    <= (type) "AxSem.res"
    1.11 -      "a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool"
    1.12 +  (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
    1.13  
    1.14  definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
    1.15   "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
     2.1 --- a/src/HOL/Bali/Basis.thy	Wed Mar 03 00:32:14 2010 +0100
     2.2 +++ b/src/HOL/Bali/Basis.thy	Wed Mar 03 00:33:02 2010 +0100
     2.3 @@ -213,11 +213,6 @@
     2.4  *}
     2.5  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
     2.6  
     2.7 -translations
     2.8 -  "option"<= (type) "Option.option"
     2.9 -  "list"  <= (type) "List.list"
    2.10 -  "sum3"  <= (type) "Basis.sum3"
    2.11 -
    2.12  
    2.13  section "quantifiers for option type"
    2.14  
     3.1 --- a/src/HOL/Bali/Decl.thy	Wed Mar 03 00:32:14 2010 +0100
     3.2 +++ b/src/HOL/Bali/Decl.thy	Wed Mar 03 00:33:02 2010 +0100
     3.3 @@ -149,24 +149,24 @@
     3.4          access :: acc_modi
     3.5  
     3.6  translations
     3.7 -  "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
     3.8 -  "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
     3.9 +  (type) "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
    3.10 +  (type) "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
    3.11  
    3.12  subsection {* Member (field or method)*}
    3.13  record  member = decl +
    3.14           static :: stat_modi
    3.15  
    3.16  translations
    3.17 -  "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
    3.18 -  "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
    3.19 +  (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
    3.20 +  (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
    3.21  
    3.22  subsection {* Field *}
    3.23  
    3.24  record field = member +
    3.25          type :: ty
    3.26  translations
    3.27 -  "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
    3.28 -  "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
    3.29 +  (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
    3.30 +  (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
    3.31  
    3.32  types     
    3.33          fdecl           (* field declaration, cf. 8.3 *)
    3.34 @@ -174,7 +174,7 @@
    3.35  
    3.36  
    3.37  translations
    3.38 -  "fdecl" <= (type) "vname \<times> field"
    3.39 +  (type) "fdecl" <= (type) "vname \<times> field"
    3.40  
    3.41  subsection  {* Method *}
    3.42  
    3.43 @@ -193,17 +193,17 @@
    3.44  
    3.45  
    3.46  translations
    3.47 -  "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
    3.48 +  (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
    3.49                        pars::vname list, resT::ty\<rparr>"
    3.50 -  "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
    3.51 +  (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
    3.52                        pars::vname list, resT::ty,\<dots>::'a\<rparr>"
    3.53 -  "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
    3.54 -  "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"      
    3.55 -  "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
    3.56 +  (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
    3.57 +  (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"      
    3.58 +  (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
    3.59                        pars::vname list, resT::ty,mbody::mbody\<rparr>"
    3.60 -  "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
    3.61 +  (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
    3.62                        pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>"
    3.63 -  "mdecl" <= (type) "sig \<times> methd"
    3.64 +  (type) "mdecl" <= (type) "sig \<times> methd"
    3.65  
    3.66  
    3.67  definition mhead :: "methd \<Rightarrow> mhead" where
    3.68 @@ -306,13 +306,13 @@
    3.69          = "qtname \<times> iface"
    3.70  
    3.71  translations
    3.72 -  "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
    3.73 -  "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
    3.74 -  "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
    3.75 +  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
    3.76 +  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
    3.77 +  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
    3.78                        isuperIfs::qtname list\<rparr>"
    3.79 -  "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
    3.80 +  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
    3.81                        isuperIfs::qtname list,\<dots>::'a\<rparr>"
    3.82 -  "idecl" <= (type) "qtname \<times> iface"
    3.83 +  (type) "idecl" <= (type) "qtname \<times> iface"
    3.84  
    3.85  definition ibody :: "iface \<Rightarrow> ibody" where
    3.86    "ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
    3.87 @@ -337,17 +337,17 @@
    3.88          = "qtname \<times> class"
    3.89  
    3.90  translations
    3.91 -  "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    3.92 +  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    3.93                        methods::mdecl list,init::stmt\<rparr>"
    3.94 -  "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    3.95 +  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    3.96                        methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
    3.97 -  "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    3.98 +  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    3.99                        methods::mdecl list,init::stmt,
   3.100                        super::qtname,superIfs::qtname list\<rparr>"
   3.101 -  "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
   3.102 +  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
   3.103                        methods::mdecl list,init::stmt,
   3.104                        super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
   3.105 -  "cdecl" <= (type) "qtname \<times> class"
   3.106 +  (type) "cdecl" <= (type) "qtname \<times> class"
   3.107  
   3.108  definition cbody :: "class \<Rightarrow> cbody" where
   3.109    "cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
   3.110 @@ -404,8 +404,8 @@
   3.111          "classes"::"cdecl list"
   3.112  
   3.113  translations
   3.114 -     "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
   3.115 -     "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
   3.116 +     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
   3.117 +     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
   3.118  
   3.119  abbreviation
   3.120    iface :: "prog  \<Rightarrow> (qtname, iface) table"
     4.1 --- a/src/HOL/Bali/DeclConcepts.thy	Wed Mar 03 00:32:14 2010 +0100
     4.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Mar 03 00:33:02 2010 +0100
     4.3 @@ -1377,7 +1377,7 @@
     4.4    fspec = "vname \<times> qtname"
     4.5  
     4.6  translations 
     4.7 -  "fspec" <= (type) "vname \<times> qtname" 
     4.8 +  (type) "fspec" <= (type) "vname \<times> qtname" 
     4.9  
    4.10  definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
    4.11  "imethds G I 
     5.1 --- a/src/HOL/Bali/Eval.thy	Wed Mar 03 00:32:14 2010 +0100
     5.2 +++ b/src/HOL/Bali/Eval.thy	Wed Mar 03 00:33:02 2010 +0100
     5.3 @@ -99,8 +99,8 @@
     5.4  types vvar  =         "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
     5.5        vals  =        "(val, vvar, val list) sum3"
     5.6  translations
     5.7 -     "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
     5.8 -     "vals" <= (type)"(val, vvar, val list) sum3" 
     5.9 +  (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
    5.10 +  (type) "vals" <= (type) "(val, vvar, val list) sum3" 
    5.11  
    5.12  text {* To avoid redundancy and to reduce the number of rules, there is only 
    5.13   one evaluation rule for each syntactic term. This is also true for variables
     6.1 --- a/src/HOL/Bali/Name.thy	Wed Mar 03 00:32:14 2010 +0100
     6.2 +++ b/src/HOL/Bali/Name.thy	Wed Mar 03 00:33:02 2010 +0100
     6.3 @@ -78,11 +78,7 @@
     6.4    qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
     6.5  
     6.6  translations
     6.7 -  "mname"  <= "Name.mname"
     6.8 -  "xname"  <= "Name.xname"
     6.9 -  "tname"  <= "Name.tname"
    6.10 -  "ename"  <= "Name.ename"
    6.11 -  "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
    6.12 +  (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
    6.13    (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
    6.14  
    6.15  
     7.1 --- a/src/HOL/Bali/State.thy	Wed Mar 03 00:32:14 2010 +0100
     7.2 +++ b/src/HOL/Bali/State.thy	Wed Mar 03 00:33:02 2010 +0100
     7.3 @@ -33,10 +33,10 @@
     7.4            "values" :: "(vn, val) table"      
     7.5  
     7.6  translations 
     7.7 -  "fspec" <= (type) "vname \<times> qtname" 
     7.8 -  "vn"    <= (type) "fspec + int"
     7.9 -  "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
    7.10 -  "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
    7.11 +  (type) "fspec" <= (type) "vname \<times> qtname" 
    7.12 +  (type) "vn"    <= (type) "fspec + int"
    7.13 +  (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
    7.14 +  (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
    7.15  
    7.16  definition the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" where
    7.17   "the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
    7.18 @@ -134,7 +134,7 @@
    7.19  translations
    7.20    "Heap" => "CONST Inl"
    7.21    "Stat" => "CONST Inr"
    7.22 -  "oref" <= (type) "loc + qtname"
    7.23 +  (type) "oref" <= (type) "loc + qtname"
    7.24  
    7.25  definition fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
    7.26   "fields_table G C P 
    7.27 @@ -213,9 +213,9 @@
    7.28          = "(lname, val) table" *) (* defined in Value.thy local variables *)
    7.29  
    7.30  translations
    7.31 - "globs"  <= (type) "(oref , obj) table"
    7.32 - "heap"   <= (type) "(loc  , obj) table"
    7.33 -(*  "locals" <= (type) "(lname, val) table" *)
    7.34 + (type) "globs"  <= (type) "(oref , obj) table"
    7.35 + (type) "heap"   <= (type) "(loc  , obj) table"
    7.36 +(*  (type) "locals" <= (type) "(lname, val) table" *)
    7.37  
    7.38  datatype st = (* pure state, i.e. contents of all variables *)
    7.39           st globs locals
    7.40 @@ -567,10 +567,8 @@
    7.41    state = "abopt \<times> st"          --{* state including abruption information *}
    7.42  
    7.43  translations
    7.44 -  "abopt"       <= (type) "State.abrupt option"
    7.45 -  "abopt"       <= (type) "abrupt option"
    7.46 -  "state"      <= (type) "abopt \<times> State.st"
    7.47 -  "state"      <= (type) "abopt \<times> st"
    7.48 +  (type) "abopt" <= (type) "abrupt option"
    7.49 +  (type) "state" <= (type) "abopt \<times> st"
    7.50  
    7.51  abbreviation
    7.52    Norm :: "st \<Rightarrow> state"
     8.1 --- a/src/HOL/Bali/Table.thy	Wed Mar 03 00:32:14 2010 +0100
     8.2 +++ b/src/HOL/Bali/Table.thy	Wed Mar 03 00:33:02 2010 +0100
     8.3 @@ -42,8 +42,7 @@
     8.4    where "table_of \<equiv> map_of"
     8.5  
     8.6  translations
     8.7 -  (type)"'a \<rightharpoonup> 'b"       <= (type)"'a \<Rightarrow> 'b Datatype.option"
     8.8 -  (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
     8.9 +  (type) "('a, 'b) table" <= (type) "'a \<rightharpoonup> 'b"
    8.10  
    8.11  (* ### To map *)
    8.12  lemma map_add_find_left[simp]:
     9.1 --- a/src/HOL/Bali/Term.thy	Wed Mar 03 00:32:14 2010 +0100
     9.2 +++ b/src/HOL/Bali/Term.thy	Wed Mar 03 00:33:02 2010 +0100
     9.3 @@ -88,7 +88,7 @@
     9.4  statement *}
     9.5  
     9.6  translations
     9.7 - "locals" <= (type) "(lname, val) table"
     9.8 + (type) "locals" <= (type) "(lname, val) table"
     9.9  
    9.10  datatype inv_mode                  --{* invocation mode for method calls *}
    9.11          = Static                   --{* static *}
    9.12 @@ -100,8 +100,8 @@
    9.13            parTs::"ty list"        
    9.14  
    9.15  translations
    9.16 -  "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
    9.17 -  "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
    9.18 +  (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
    9.19 +  (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
    9.20  
    9.21  --{* function codes for unary operations *}
    9.22  datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
    9.23 @@ -237,11 +237,8 @@
    9.24   
    9.25  types "term" = "(expr+stmt,var,expr list) sum3"
    9.26  translations
    9.27 -  "sig"   <= (type) "mname \<times> ty list"
    9.28 -  "var"   <= (type) "Term.var"
    9.29 -  "expr"  <= (type) "Term.expr"
    9.30 -  "stmt"  <= (type) "Term.stmt"
    9.31 -  "term"  <= (type) "(expr+stmt,var,expr list) sum3"
    9.32 +  (type) "sig"   <= (type) "mname \<times> ty list"
    9.33 +  (type) "term"  <= (type) "(expr+stmt,var,expr list) sum3"
    9.34  
    9.35  abbreviation this :: expr
    9.36    where "this == Acc (LVar This)"
    10.1 --- a/src/HOL/Bali/Type.thy	Wed Mar 03 00:32:14 2010 +0100
    10.2 +++ b/src/HOL/Bali/Type.thy	Wed Mar 03 00:33:02 2010 +0100
    10.3 @@ -30,11 +30,6 @@
    10.4          = PrimT prim_ty --{* primitive type *}
    10.5          | RefT  ref_ty  --{* reference type *}
    10.6  
    10.7 -translations
    10.8 -  "prim_ty" <= (type) "Type.prim_ty"
    10.9 -  "ref_ty"  <= (type) "Type.ref_ty"
   10.10 -  "ty"      <= (type) "Type.ty"
   10.11 -
   10.12  abbreviation "NT == RefT NullT"
   10.13  abbreviation "Iface I == RefT (IfaceT I)"
   10.14  abbreviation "Class C == RefT (ClassT C)"
    11.1 --- a/src/HOL/Bali/Value.thy	Wed Mar 03 00:32:14 2010 +0100
    11.2 +++ b/src/HOL/Bali/Value.thy	Wed Mar 03 00:33:02 2010 +0100
    11.3 @@ -17,9 +17,6 @@
    11.4          | Addr loc      --{* addresses, i.e. locations of objects *}
    11.5  
    11.6  
    11.7 -translations "val" <= (type) "Term.val"
    11.8 -             "loc" <= (type) "Term.loc"
    11.9 -
   11.10  consts   the_Bool   :: "val \<Rightarrow> bool"  
   11.11  primrec "the_Bool (Bool b) = b"
   11.12  consts   the_Intg   :: "val \<Rightarrow> int"
    12.1 --- a/src/HOL/Bali/WellType.thy	Wed Mar 03 00:32:14 2010 +0100
    12.2 +++ b/src/HOL/Bali/WellType.thy	Wed Mar 03 00:33:02 2010 +0100
    12.3 @@ -37,10 +37,10 @@
    12.4           lcl:: "lenv"    --{* local environment *}     
    12.5    
    12.6  translations
    12.7 -  "lenv" <= (type) "(lname, ty) table"
    12.8 -  "lenv" <= (type) "lname \<Rightarrow> ty option"
    12.9 -  "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
   12.10 -  "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
   12.11 +  (type) "lenv" <= (type) "(lname, ty) table"
   12.12 +  (type) "lenv" <= (type) "lname \<Rightarrow> ty option"
   12.13 +  (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
   12.14 +  (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
   12.15  
   12.16  
   12.17  abbreviation
   12.18 @@ -238,9 +238,9 @@
   12.19  
   12.20  section "Typing for terms"
   12.21  
   12.22 -types tys  =        "ty + ty list"
   12.23 +types tys  = "ty + ty list"
   12.24  translations
   12.25 -  "tys"   <= (type) "ty + ty list"
   12.26 +  (type) "tys" <= (type) "ty + ty list"
   12.27  
   12.28  
   12.29  inductive
    13.1 --- a/src/HOL/IMPP/Hoare.thy	Wed Mar 03 00:32:14 2010 +0100
    13.2 +++ b/src/HOL/IMPP/Hoare.thy	Wed Mar 03 00:33:02 2010 +0100
    13.3 @@ -18,7 +18,7 @@
    13.4  
    13.5  types 'a assn = "'a => state => bool"
    13.6  translations
    13.7 -  "a assn"   <= (type)"a => state => bool"
    13.8 +  (type) "'a assn" <= (type) "'a => state => bool"
    13.9  
   13.10  definition
   13.11    state_not_singleton :: bool where
    14.1 --- a/src/HOL/Library/Numeral_Type.thy	Wed Mar 03 00:32:14 2010 +0100
    14.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Mar 03 00:33:02 2010 +0100
    14.3 @@ -32,7 +32,7 @@
    14.4  
    14.5  syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    14.6  
    14.7 -translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
    14.8 +translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
    14.9  
   14.10  typed_print_translation {*
   14.11  let
    15.1 --- a/src/HOL/MicroJava/J/Decl.thy	Wed Mar 03 00:32:14 2010 +0100
    15.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Wed Mar 03 00:33:02 2010 +0100
    15.3 @@ -23,12 +23,12 @@
    15.4  
    15.5  
    15.6  translations
    15.7 -  "fdecl"   <= (type) "vname \<times> ty"
    15.8 -  "sig"     <= (type) "mname \<times> ty list"
    15.9 -  "mdecl c" <= (type) "sig \<times> ty \<times> c"
   15.10 -  "class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list"
   15.11 -  "cdecl c" <= (type) "cname \<times> (c class)"
   15.12 -  "prog  c" <= (type) "(c cdecl) list"
   15.13 +  (type) "fdecl" <= (type) "vname \<times> ty"
   15.14 +  (type) "sig" <= (type) "mname \<times> ty list"
   15.15 +  (type) "'c mdecl" <= (type) "sig \<times> ty \<times> 'c"
   15.16 +  (type) "'c class" <= (type) "cname \<times> fdecl list \<times> ('c mdecl) list"
   15.17 +  (type) "'c cdecl" <= (type) "cname \<times> ('c class)"
   15.18 +  (type) "'c prog" <= (type) "('c cdecl) list"
   15.19  
   15.20  
   15.21  definition "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" where
    16.1 --- a/src/HOL/NanoJava/AxSem.thy	Wed Mar 03 00:32:14 2010 +0100
    16.2 +++ b/src/HOL/NanoJava/AxSem.thy	Wed Mar 03 00:33:02 2010 +0100
    16.3 @@ -13,10 +13,10 @@
    16.4        triple = "assn \<times> stmt \<times>  assn"
    16.5       etriple = "assn \<times> expr \<times> vassn"
    16.6  translations
    16.7 -  "assn"   \<leftharpoondown> (type)"state => bool"
    16.8 - "vassn"   \<leftharpoondown> (type)"val => assn"
    16.9 -  "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times>  assn"
   16.10 - "etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
   16.11 +  (type) "assn" \<leftharpoondown> (type) "state => bool"
   16.12 +  (type) "vassn" \<leftharpoondown> (type) "val => assn"
   16.13 +  (type) "triple" \<leftharpoondown> (type) "assn \<times> stmt \<times> assn"
   16.14 +  (type) "etriple" \<leftharpoondown> (type) "assn \<times> expr \<times> vassn"
   16.15  
   16.16  
   16.17  subsection "Hoare Logic Rules"
    17.1 --- a/src/HOL/NanoJava/Decl.thy	Wed Mar 03 00:32:14 2010 +0100
    17.2 +++ b/src/HOL/NanoJava/Decl.thy	Wed Mar 03 00:33:02 2010 +0100
    17.3 @@ -38,11 +38,11 @@
    17.4          = "cdecl list"
    17.5  
    17.6  translations
    17.7 -  "fdecl" \<leftharpoondown> (type)"fname \<times> ty"
    17.8 -  "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
    17.9 -  "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
   17.10 -  "cdecl" \<leftharpoondown> (type)"cname \<times> class"
   17.11 -  "prog " \<leftharpoondown> (type)"cdecl list"
   17.12 +  (type) "fdecl" \<leftharpoondown> (type) "fname \<times> ty"
   17.13 +  (type) "mdecl" \<leftharpoondown> (type) "mname \<times> ty \<times> ty \<times> stmt"
   17.14 +  (type) "class" \<leftharpoondown> (type) "cname \<times> fdecl list \<times> mdecl list"
   17.15 +  (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class"
   17.16 +  (type) "prog " \<leftharpoondown> (type) "cdecl list"
   17.17  
   17.18  consts
   17.19  
    18.1 --- a/src/HOL/NanoJava/State.thy	Wed Mar 03 00:32:14 2010 +0100
    18.2 +++ b/src/HOL/NanoJava/State.thy	Wed Mar 03 00:33:02 2010 +0100
    18.3 @@ -23,9 +23,8 @@
    18.4          obj = "cname \<times> fields"
    18.5  
    18.6  translations
    18.7 -
    18.8 -  "fields" \<leftharpoondown> (type)"fname => val option"
    18.9 -  "obj"    \<leftharpoondown> (type)"cname \<times> fields"
   18.10 +  (type) "fields" \<leftharpoondown> (type) "fname => val option"
   18.11 +  (type) "obj"    \<leftharpoondown> (type) "cname \<times> fields"
   18.12  
   18.13  definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where
   18.14   "init_vars m == Option.map (\<lambda>T. Null) o m"
   18.15 @@ -40,10 +39,9 @@
   18.16            locals :: locals
   18.17  
   18.18  translations
   18.19 -
   18.20 -  "heap"   \<leftharpoondown> (type)"loc   => obj option"
   18.21 -  "locals" \<leftharpoondown> (type)"vname => val option"
   18.22 -  "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"
   18.23 +  (type) "heap" \<leftharpoondown> (type) "loc => obj option"
   18.24 +  (type) "locals" \<leftharpoondown> (type) "vname => val option"
   18.25 +  (type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)"
   18.26  
   18.27  definition del_locs :: "state => state" where
   18.28   "del_locs s \<equiv> s (| locals := empty |)"
    19.1 --- a/src/HOLCF/One.thy	Wed Mar 03 00:32:14 2010 +0100
    19.2 +++ b/src/HOLCF/One.thy	Wed Mar 03 00:33:02 2010 +0100
    19.3 @@ -10,7 +10,7 @@
    19.4  
    19.5  types one = "unit lift"
    19.6  translations
    19.7 -  "one" <= (type) "unit lift" 
    19.8 +  (type) "one" <= (type) "unit lift" 
    19.9  
   19.10  definition
   19.11    ONE :: "one"
    20.1 --- a/src/HOLCF/Representable.thy	Wed Mar 03 00:32:14 2010 +0100
    20.2 +++ b/src/HOLCF/Representable.thy	Wed Mar 03 00:33:02 2010 +0100
    20.3 @@ -49,7 +49,7 @@
    20.4  text "A TypeRep is an algebraic deflation over the universe of values."
    20.5  
    20.6  types TypeRep = "udom alg_defl"
    20.7 -translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
    20.8 +translations (type) "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
    20.9  
   20.10  definition
   20.11    Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
   20.12 @@ -59,7 +59,7 @@
   20.13        (emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
   20.14  
   20.15  syntax "_REP" :: "type \<Rightarrow> TypeRep"  ("(1REP/(1'(_')))")
   20.16 -translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)"
   20.17 +translations "REP('t)" \<rightleftharpoons> "CONST Rep_of TYPE('t)"
   20.18  
   20.19  lemma cast_REP:
   20.20    "cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"
    21.1 --- a/src/HOLCF/Tr.thy	Wed Mar 03 00:32:14 2010 +0100
    21.2 +++ b/src/HOLCF/Tr.thy	Wed Mar 03 00:33:02 2010 +0100
    21.3 @@ -14,7 +14,7 @@
    21.4    tr = "bool lift"
    21.5  
    21.6  translations
    21.7 -  "tr" <= (type) "bool lift"
    21.8 +  (type) "tr" <= (type) "bool lift"
    21.9  
   21.10  definition
   21.11    TT :: "tr" where