--- a/src/HOL/Bali/AxSem.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/AxSem.thy Wed Mar 03 00:33:02 2010 +0100
@@ -58,10 +58,9 @@
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> CONST the_In3"
--{* relation on result values, state and auxiliary variables *}
-types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
+types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
translations
- "res" <= (type) "AxSem.res"
- "a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool"
+ (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
"P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
--- a/src/HOL/Bali/Basis.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Basis.thy Wed Mar 03 00:33:02 2010 +0100
@@ -213,11 +213,6 @@
*}
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
-translations
- "option"<= (type) "Option.option"
- "list" <= (type) "List.list"
- "sum3" <= (type) "Basis.sum3"
-
section "quantifiers for option type"
--- a/src/HOL/Bali/Decl.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Decl.thy Wed Mar 03 00:33:02 2010 +0100
@@ -149,24 +149,24 @@
access :: acc_modi
translations
- "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
- "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
+ (type) "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
+ (type) "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
subsection {* Member (field or method)*}
record member = decl +
static :: stat_modi
translations
- "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
- "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
+ (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
+ (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
subsection {* Field *}
record field = member +
type :: ty
translations
- "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
- "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
+ (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
+ (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
types
fdecl (* field declaration, cf. 8.3 *)
@@ -174,7 +174,7 @@
translations
- "fdecl" <= (type) "vname \<times> field"
+ (type) "fdecl" <= (type) "vname \<times> field"
subsection {* Method *}
@@ -193,17 +193,17 @@
translations
- "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty\<rparr>"
- "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty,\<dots>::'a\<rparr>"
- "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
- "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"
- "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
+ (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"
+ (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty,mbody::mbody\<rparr>"
- "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>"
- "mdecl" <= (type) "sig \<times> methd"
+ (type) "mdecl" <= (type) "sig \<times> methd"
definition mhead :: "methd \<Rightarrow> mhead" where
@@ -306,13 +306,13 @@
= "qtname \<times> iface"
translations
- "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
- "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
- "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
+ (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
+ (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
+ (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
isuperIfs::qtname list\<rparr>"
- "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
+ (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
isuperIfs::qtname list,\<dots>::'a\<rparr>"
- "idecl" <= (type) "qtname \<times> iface"
+ (type) "idecl" <= (type) "qtname \<times> iface"
definition ibody :: "iface \<Rightarrow> ibody" where
"ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
@@ -337,17 +337,17 @@
= "qtname \<times> class"
translations
- "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt\<rparr>"
- "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
- "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt,
super::qtname,superIfs::qtname list\<rparr>"
- "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt,
super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
- "cdecl" <= (type) "qtname \<times> class"
+ (type) "cdecl" <= (type) "qtname \<times> class"
definition cbody :: "class \<Rightarrow> cbody" where
"cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
@@ -404,8 +404,8 @@
"classes"::"cdecl list"
translations
- "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
- "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
+ (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
+ (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
abbreviation
iface :: "prog \<Rightarrow> (qtname, iface) table"
--- a/src/HOL/Bali/DeclConcepts.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Wed Mar 03 00:33:02 2010 +0100
@@ -1377,7 +1377,7 @@
fspec = "vname \<times> qtname"
translations
- "fspec" <= (type) "vname \<times> qtname"
+ (type) "fspec" <= (type) "vname \<times> qtname"
definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
"imethds G I
--- a/src/HOL/Bali/Eval.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Eval.thy Wed Mar 03 00:33:02 2010 +0100
@@ -99,8 +99,8 @@
types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
vals = "(val, vvar, val list) sum3"
translations
- "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
- "vals" <= (type)"(val, vvar, val list) sum3"
+ (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
+ (type) "vals" <= (type) "(val, vvar, val list) sum3"
text {* To avoid redundancy and to reduce the number of rules, there is only
one evaluation rule for each syntactic term. This is also true for variables
--- a/src/HOL/Bali/Name.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Name.thy Wed Mar 03 00:33:02 2010 +0100
@@ -78,11 +78,7 @@
qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
translations
- "mname" <= "Name.mname"
- "xname" <= "Name.xname"
- "tname" <= "Name.tname"
- "ename" <= "Name.ename"
- "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
+ (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
(type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
--- a/src/HOL/Bali/State.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/State.thy Wed Mar 03 00:33:02 2010 +0100
@@ -33,10 +33,10 @@
"values" :: "(vn, val) table"
translations
- "fspec" <= (type) "vname \<times> qtname"
- "vn" <= (type) "fspec + int"
- "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
- "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
+ (type) "fspec" <= (type) "vname \<times> qtname"
+ (type) "vn" <= (type) "fspec + int"
+ (type) "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
+ (type) "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
definition the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" where
"the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
@@ -134,7 +134,7 @@
translations
"Heap" => "CONST Inl"
"Stat" => "CONST Inr"
- "oref" <= (type) "loc + qtname"
+ (type) "oref" <= (type) "loc + qtname"
definition fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table" where
"fields_table G C P
@@ -213,9 +213,9 @@
= "(lname, val) table" *) (* defined in Value.thy local variables *)
translations
- "globs" <= (type) "(oref , obj) table"
- "heap" <= (type) "(loc , obj) table"
-(* "locals" <= (type) "(lname, val) table" *)
+ (type) "globs" <= (type) "(oref , obj) table"
+ (type) "heap" <= (type) "(loc , obj) table"
+(* (type) "locals" <= (type) "(lname, val) table" *)
datatype st = (* pure state, i.e. contents of all variables *)
st globs locals
@@ -567,10 +567,8 @@
state = "abopt \<times> st" --{* state including abruption information *}
translations
- "abopt" <= (type) "State.abrupt option"
- "abopt" <= (type) "abrupt option"
- "state" <= (type) "abopt \<times> State.st"
- "state" <= (type) "abopt \<times> st"
+ (type) "abopt" <= (type) "abrupt option"
+ (type) "state" <= (type) "abopt \<times> st"
abbreviation
Norm :: "st \<Rightarrow> state"
--- a/src/HOL/Bali/Table.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Table.thy Wed Mar 03 00:33:02 2010 +0100
@@ -42,8 +42,7 @@
where "table_of \<equiv> map_of"
translations
- (type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option"
- (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
+ (type) "('a, 'b) table" <= (type) "'a \<rightharpoonup> 'b"
(* ### To map *)
lemma map_add_find_left[simp]:
--- a/src/HOL/Bali/Term.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Term.thy Wed Mar 03 00:33:02 2010 +0100
@@ -88,7 +88,7 @@
statement *}
translations
- "locals" <= (type) "(lname, val) table"
+ (type) "locals" <= (type) "(lname, val) table"
datatype inv_mode --{* invocation mode for method calls *}
= Static --{* static *}
@@ -100,8 +100,8 @@
parTs::"ty list"
translations
- "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
- "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
+ (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
+ (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
--{* function codes for unary operations *}
datatype unop = UPlus -- {*{\tt +} unary plus*}
@@ -237,11 +237,8 @@
types "term" = "(expr+stmt,var,expr list) sum3"
translations
- "sig" <= (type) "mname \<times> ty list"
- "var" <= (type) "Term.var"
- "expr" <= (type) "Term.expr"
- "stmt" <= (type) "Term.stmt"
- "term" <= (type) "(expr+stmt,var,expr list) sum3"
+ (type) "sig" <= (type) "mname \<times> ty list"
+ (type) "term" <= (type) "(expr+stmt,var,expr list) sum3"
abbreviation this :: expr
where "this == Acc (LVar This)"
--- a/src/HOL/Bali/Type.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Type.thy Wed Mar 03 00:33:02 2010 +0100
@@ -30,11 +30,6 @@
= PrimT prim_ty --{* primitive type *}
| RefT ref_ty --{* reference type *}
-translations
- "prim_ty" <= (type) "Type.prim_ty"
- "ref_ty" <= (type) "Type.ref_ty"
- "ty" <= (type) "Type.ty"
-
abbreviation "NT == RefT NullT"
abbreviation "Iface I == RefT (IfaceT I)"
abbreviation "Class C == RefT (ClassT C)"
--- a/src/HOL/Bali/Value.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Value.thy Wed Mar 03 00:33:02 2010 +0100
@@ -17,9 +17,6 @@
| Addr loc --{* addresses, i.e. locations of objects *}
-translations "val" <= (type) "Term.val"
- "loc" <= (type) "Term.loc"
-
consts the_Bool :: "val \<Rightarrow> bool"
primrec "the_Bool (Bool b) = b"
consts the_Intg :: "val \<Rightarrow> int"
--- a/src/HOL/Bali/WellType.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/WellType.thy Wed Mar 03 00:33:02 2010 +0100
@@ -37,10 +37,10 @@
lcl:: "lenv" --{* local environment *}
translations
- "lenv" <= (type) "(lname, ty) table"
- "lenv" <= (type) "lname \<Rightarrow> ty option"
- "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
- "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
+ (type) "lenv" <= (type) "(lname, ty) table"
+ (type) "lenv" <= (type) "lname \<Rightarrow> ty option"
+ (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
+ (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
abbreviation
@@ -238,9 +238,9 @@
section "Typing for terms"
-types tys = "ty + ty list"
+types tys = "ty + ty list"
translations
- "tys" <= (type) "ty + ty list"
+ (type) "tys" <= (type) "ty + ty list"
inductive
--- a/src/HOL/IMPP/Hoare.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/IMPP/Hoare.thy Wed Mar 03 00:33:02 2010 +0100
@@ -18,7 +18,7 @@
types 'a assn = "'a => state => bool"
translations
- "a assn" <= (type)"a => state => bool"
+ (type) "'a assn" <= (type) "'a => state => bool"
definition
state_not_singleton :: bool where
--- a/src/HOL/Library/Numeral_Type.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Wed Mar 03 00:33:02 2010 +0100
@@ -32,7 +32,7 @@
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
-translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
+translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
typed_print_translation {*
let
--- a/src/HOL/MicroJava/J/Decl.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Wed Mar 03 00:33:02 2010 +0100
@@ -23,12 +23,12 @@
translations
- "fdecl" <= (type) "vname \<times> ty"
- "sig" <= (type) "mname \<times> ty list"
- "mdecl c" <= (type) "sig \<times> ty \<times> c"
- "class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list"
- "cdecl c" <= (type) "cname \<times> (c class)"
- "prog c" <= (type) "(c cdecl) list"
+ (type) "fdecl" <= (type) "vname \<times> ty"
+ (type) "sig" <= (type) "mname \<times> ty list"
+ (type) "'c mdecl" <= (type) "sig \<times> ty \<times> 'c"
+ (type) "'c class" <= (type) "cname \<times> fdecl list \<times> ('c mdecl) list"
+ (type) "'c cdecl" <= (type) "cname \<times> ('c class)"
+ (type) "'c prog" <= (type) "('c cdecl) list"
definition "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" where
--- a/src/HOL/NanoJava/AxSem.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/NanoJava/AxSem.thy Wed Mar 03 00:33:02 2010 +0100
@@ -13,10 +13,10 @@
triple = "assn \<times> stmt \<times> assn"
etriple = "assn \<times> expr \<times> vassn"
translations
- "assn" \<leftharpoondown> (type)"state => bool"
- "vassn" \<leftharpoondown> (type)"val => assn"
- "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
- "etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
+ (type) "assn" \<leftharpoondown> (type) "state => bool"
+ (type) "vassn" \<leftharpoondown> (type) "val => assn"
+ (type) "triple" \<leftharpoondown> (type) "assn \<times> stmt \<times> assn"
+ (type) "etriple" \<leftharpoondown> (type) "assn \<times> expr \<times> vassn"
subsection "Hoare Logic Rules"
--- a/src/HOL/NanoJava/Decl.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/NanoJava/Decl.thy Wed Mar 03 00:33:02 2010 +0100
@@ -38,11 +38,11 @@
= "cdecl list"
translations
- "fdecl" \<leftharpoondown> (type)"fname \<times> ty"
- "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
- "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
- "cdecl" \<leftharpoondown> (type)"cname \<times> class"
- "prog " \<leftharpoondown> (type)"cdecl list"
+ (type) "fdecl" \<leftharpoondown> (type) "fname \<times> ty"
+ (type) "mdecl" \<leftharpoondown> (type) "mname \<times> ty \<times> ty \<times> stmt"
+ (type) "class" \<leftharpoondown> (type) "cname \<times> fdecl list \<times> mdecl list"
+ (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class"
+ (type) "prog " \<leftharpoondown> (type) "cdecl list"
consts
--- a/src/HOL/NanoJava/State.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/NanoJava/State.thy Wed Mar 03 00:33:02 2010 +0100
@@ -23,9 +23,8 @@
obj = "cname \<times> fields"
translations
-
- "fields" \<leftharpoondown> (type)"fname => val option"
- "obj" \<leftharpoondown> (type)"cname \<times> fields"
+ (type) "fields" \<leftharpoondown> (type) "fname => val option"
+ (type) "obj" \<leftharpoondown> (type) "cname \<times> fields"
definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where
"init_vars m == Option.map (\<lambda>T. Null) o m"
@@ -40,10 +39,9 @@
locals :: locals
translations
-
- "heap" \<leftharpoondown> (type)"loc => obj option"
- "locals" \<leftharpoondown> (type)"vname => val option"
- "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"
+ (type) "heap" \<leftharpoondown> (type) "loc => obj option"
+ (type) "locals" \<leftharpoondown> (type) "vname => val option"
+ (type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)"
definition del_locs :: "state => state" where
"del_locs s \<equiv> s (| locals := empty |)"
--- a/src/HOLCF/One.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOLCF/One.thy Wed Mar 03 00:33:02 2010 +0100
@@ -10,7 +10,7 @@
types one = "unit lift"
translations
- "one" <= (type) "unit lift"
+ (type) "one" <= (type) "unit lift"
definition
ONE :: "one"
--- a/src/HOLCF/Representable.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOLCF/Representable.thy Wed Mar 03 00:33:02 2010 +0100
@@ -49,7 +49,7 @@
text "A TypeRep is an algebraic deflation over the universe of values."
types TypeRep = "udom alg_defl"
-translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
+translations (type) "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
definition
Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
@@ -59,7 +59,7 @@
(emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
syntax "_REP" :: "type \<Rightarrow> TypeRep" ("(1REP/(1'(_')))")
-translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)"
+translations "REP('t)" \<rightleftharpoons> "CONST Rep_of TYPE('t)"
lemma cast_REP:
"cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"
--- a/src/HOLCF/Tr.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOLCF/Tr.thy Wed Mar 03 00:33:02 2010 +0100
@@ -14,7 +14,7 @@
tr = "bool lift"
translations
- "tr" <= (type) "bool lift"
+ (type) "tr" <= (type) "bool lift"
definition
TT :: "tr" where