--- a/src/HOL/Hoare/HeapSyntax.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/Hoare/HeapSyntax.thy Thu Feb 11 08:44:41 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/HeapSyntax.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TUM
*)
@@ -9,16 +8,16 @@
subsection "Field access and update"
syntax
- "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
+ "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
("_/'((_ \<rightarrow> _)')" [1000,0] 900)
- "@fassign" :: "'a ref => id => 'v => 's com"
+ "_fassign" :: "'a ref => id => 'v => 's com"
("(2_^._ :=/ _)" [70,1000,65] 61)
- "@faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
+ "_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
("_^._" [65,1000] 65)
translations
- "f(r \<rightarrow> v)" == "f(addr r := v)"
+ "f(r \<rightarrow> v)" == "f(CONST addr r := v)"
"p^.f := e" => "f := f(p \<rightarrow> e)"
- "p^.f" => "f(addr p)"
+ "p^.f" => "f(CONST addr p)"
declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Thu Feb 11 08:44:41 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/HeapSyntax.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TUM
*)
@@ -17,16 +16,16 @@
reason about storage allocation/deallocation. *}
syntax
- "refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
+ "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
("_/'((_ \<rightarrow> _)')" [1000,0] 900)
- "@fassign" :: "'a ref => id => 'v => 's com"
+ "_fassign" :: "'a ref => id => 'v => 's com"
("(2_^._ :=/ _)" [70,1000,65] 61)
- "@faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
+ "_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
("_^._" [65,1000] 65)
translations
- "refupdate f r v" == "f(addr r := v)"
- "p^.f := e" => "(p \<noteq> Null) \<rightarrow> (f := refupdate f p e)"
- "p^.f" => "f(addr p)"
+ "_refupdate f r v" == "f(CONST addr r := v)"
+ "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
+ "p^.f" => "f(CONST addr p)"
declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
--- a/src/HOL/Hoare/HoareAbort.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy Thu Feb 11 08:44:41 2010 +0100
@@ -257,7 +257,7 @@
guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61)
translations
- "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
+ "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
"a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
(* reverse translation not possible because of duplicate "a" *)
--- a/src/HOL/Hoare/Pointers0.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/Hoare/Pointers0.thy Thu Feb 11 08:44:41 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/Pointers.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TUM
@@ -20,12 +19,12 @@
subsection "Field access and update"
syntax
- "@fassign" :: "'a::ref => id => 'v => 's com"
+ "_fassign" :: "'a::ref => id => 'v => 's com"
("(2_^._ :=/ _)" [70,1000,65] 61)
- "@faccess" :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
+ "_faccess" :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
("_^._" [65,1000] 65)
translations
- "p^.f := e" => "f := fun_upd f p e"
+ "p^.f := e" => "f := CONST fun_upd f p e"
"p^.f" => "f p"
--- a/src/HOL/Hoare/Separation.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/Hoare/Separation.thy Thu Feb 11 08:44:41 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/Separation.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2003 TUM
@@ -50,10 +49,10 @@
bound Hs - otherwise they may bind the implicit H. *}
syntax
- "@emp" :: "bool" ("emp")
- "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
- "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
- "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
+ "_emp" :: "bool" ("emp")
+ "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
+ "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
+ "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
(* FIXME does not handle "_idtdummy" *)
ML{*
@@ -79,8 +78,8 @@
*}
parse_translation
- {* [("@emp", emp_tr), ("@singl", singl_tr),
- ("@star", star_tr), ("@wand", wand_tr)] *}
+ {* [("_emp", emp_tr), ("_singl", singl_tr),
+ ("_star", star_tr), ("_wand", wand_tr)] *}
text{* Now it looks much better: *}
@@ -121,13 +120,13 @@
*)
| strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
| strip (Abs(_,_,P)) = P
- | strip (Const("is_empty",_)) = Syntax.const "@emp"
+ | strip (Const("is_empty",_)) = Syntax.const "_emp"
| strip t = t;
in
-fun is_empty_tr' [_] = Syntax.const "@emp"
-fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q
-fun star_tr' [P,Q,_] = Syntax.const "@star" $ strip P $ strip Q
-fun wand_tr' [P,Q,_] = Syntax.const "@wand" $ strip P $ strip Q
+fun is_empty_tr' [_] = Syntax.const "_emp"
+fun singl_tr' [_,p,q] = Syntax.const "_singl" $ p $ q
+fun star_tr' [P,Q,_] = Syntax.const "_star" $ strip P $ strip Q
+fun wand_tr' [P,Q,_] = Syntax.const "_wand" $ strip P $ strip Q
end
*}
--- a/src/HOL/MicroJava/BV/BVExample.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Thu Feb 11 08:44:41 2010 +0100
@@ -296,12 +296,10 @@
done
text {* Some abbreviations for readability *}
-syntax
- Clist :: ty
- Ctest :: ty
-translations
- "Clist" == "Class list_name"
- "Ctest" == "Class test_name"
+abbreviation Clist :: ty
+ where "Clist == Class list_name"
+abbreviation Ctest :: ty
+ where "Ctest == Class test_name"
constdefs
phi_makelist :: method_type ("\<phi>\<^sub>m")
--- a/src/HOL/MicroJava/BV/JType.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Thu Feb 11 08:44:41 2010 +0100
@@ -37,9 +37,7 @@
"is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow>
(case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C, Object) \<in> (subcls1 G)^*)"
-
-translations
- "types G" == "Collect (is_type G)"
+abbreviation "types G == Collect (is_type G)"
constdefs
esl :: "'c prog \<Rightarrow> ty esl"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Feb 11 08:44:41 2010 +0100
@@ -584,10 +584,9 @@
(* Currently: empty exception_table *)
-syntax
+abbreviation (input)
empty_et :: exception_table
-translations
- "empty_et" => "[]"
+ where "empty_et == []"
@@ -860,12 +859,13 @@
section "Correspondence bytecode - method types"
(* ********************************************************************** *)
-syntax
+abbreviation (input)
ST_of :: "state_type \<Rightarrow> opstack_type"
+ where "ST_of == fst"
+
+abbreviation (input)
LT_of :: "state_type \<Rightarrow> locvars_type"
-translations
- "ST_of" => "fst"
- "LT_of" => "snd"
+ where "LT_of == snd"
lemma states_lower:
"\<lbrakk> OK (Some (ST, LT)) \<in> states cG mxs mxr; length ST \<le> mxs\<rbrakk>
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Feb 11 08:44:41 2010 +0100
@@ -262,10 +262,8 @@
done
-syntax
- mtd_mb :: "cname \<times> ty \<times> 'c \<Rightarrow> 'c"
-translations
- "mtd_mb" => "Fun.comp snd snd"
+abbreviation (input)
+ "mtd_mb == snd o snd"
lemma map_of_map_fst: "\<lbrakk> inj f;
\<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Thu Feb 11 08:44:41 2010 +0100
@@ -41,13 +41,13 @@
(**********************************************************************)
-syntax
- mt_of :: "method_type \<times> state_type \<Rightarrow> method_type"
- sttp_of :: "method_type \<times> state_type \<Rightarrow> state_type"
+abbreviation (input)
+ mt_of :: "method_type \<times> state_type \<Rightarrow> method_type"
+ where "mt_of == fst"
-translations
- "mt_of" => "fst"
- "sttp_of" => "snd"
+abbreviation (input)
+ sttp_of :: "method_type \<times> state_type \<Rightarrow> state_type"
+ where "sttp_of == snd"
consts
compTpExpr :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr
@@ -189,4 +189,3 @@
end
-
--- a/src/HOL/MicroJava/DFA/Err.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Err.thy Thu Feb 11 08:44:41 2010 +0100
@@ -45,10 +45,9 @@
sl :: "'a esl \<Rightarrow> 'a err sl"
"sl == %(A,r,f). (err A, le r, lift2 f)"
-syntax
- err_semilat :: "'a esl \<Rightarrow> bool"
-translations
-"err_semilat L" == "semilat(Err.sl L)"
+abbreviation
+ err_semilat :: "'a esl \<Rightarrow> bool"
+ where "err_semilat L == semilat(Err.sl L)"
consts
--- a/src/HOL/MicroJava/DFA/Listn.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy Thu Feb 11 08:44:41 2010 +0100
@@ -17,21 +17,24 @@
le :: "'a ord \<Rightarrow> ('a list)ord"
"le r == list_all2 (%x y. x <=_r y)"
-syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
+abbreviation
+ lesublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
("(_ /<=[_] _)" [50, 0, 51] 50)
-syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "x <=[r] y == x <=_(le r) y"
+
+abbreviation
+ lesssublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
("(_ /<[_] _)" [50, 0, 51] 50)
-translations
- "x <=[r] y" == "x <=_(Listn.le r) y"
- "x <[r] y" == "x <_(Listn.le r) y"
+ where "x <[r] y == x <_(le r) y"
constdefs
map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
"map2 f == (%xs ys. map (split f) (zip xs ys))"
-syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
+abbreviation
+ plussublist_syntax :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
("(_ /+[_] _)" [65, 0, 66] 65)
-translations "x +[f] y" == "x +_(map2 f) y"
+ where "x +[f] y == x +_(map2 f) y"
consts coalesce :: "'a err list \<Rightarrow> 'a list err"
primrec
--- a/src/HOL/MicroJava/J/Example.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Thu Feb 11 08:44:41 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/J/Example.thy
- ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
*)
@@ -55,19 +54,16 @@
declare inj_cnam' [simp] inj_vnam' [simp]
-syntax
- Base :: cname
- Ext :: cname
- vee :: vname
- x :: vname
- e :: vname
-
-translations
- "Base" == "cnam' Base'"
- "Ext" == "cnam' Ext'"
- "vee" == "VName (vnam' vee')"
- "x" == "VName (vnam' x')"
- "e" == "VName (vnam' e')"
+abbreviation Base :: cname
+ where "Base == cnam' Base'"
+abbreviation Ext :: cname
+ where "Ext == cnam' Ext'"
+abbreviation vee :: vname
+ where "vee == VName (vnam' vee')"
+abbreviation x :: vname
+ where "x == VName (vnam' x')"
+abbreviation e :: vname
+ where "e == VName (vnam' e')"
axioms
Base_not_Object: "Base \<noteq> Object"
--- a/src/HOL/MicroJava/J/Exceptions.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/J/Exceptions.thy Thu Feb 11 08:44:41 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/J/Exceptions.thy
- ID: $Id$
Author: Gerwin Klein, Martin Strecker
Copyright 2002 Technische Universitaet Muenchen
*)
@@ -17,11 +16,9 @@
(XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
-consts
+abbreviation
cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname"
-
-translations
- "cname_of hp v" == "fst (CONST the (hp (the_Addr v)))"
+ where "cname_of hp v == fst (the (hp (the_Addr v)))"
constdefs
--- a/src/HOL/MicroJava/J/State.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/J/State.thy Thu Feb 11 08:44:41 2010 +0100
@@ -27,21 +27,27 @@
state = "aheap \<times> locals" -- "heap, local parameter including This"
xstate = "val option \<times> state" -- "state including exception information"
-syntax
- heap :: "state => aheap"
- locals :: "state => locals"
- Norm :: "state => xstate"
- abrupt :: "xstate \<Rightarrow> val option"
- store :: "xstate \<Rightarrow> state"
- lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj"
+abbreviation (input)
+ heap :: "state => aheap"
+ where "heap == fst"
+
+abbreviation (input)
+ locals :: "state => locals"
+ where "locals == snd"
+
+abbreviation "Norm s == (None, s)"
-translations
- "heap" => "fst"
- "locals" => "snd"
- "Norm s" == "(None,s)"
- "abrupt" => "fst"
- "store" => "snd"
- "lookup_obj s a'" == "CONST the (heap s (the_Addr a'))"
+abbreviation (input)
+ abrupt :: "xstate \<Rightarrow> val option"
+ where "abrupt == fst"
+
+abbreviation (input)
+ store :: "xstate \<Rightarrow> state"
+ where "store == snd"
+
+abbreviation
+ lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj"
+ where "lookup_obj s a' == the (heap s (the_Addr a'))"
constdefs
--- a/src/HOL/MicroJava/J/Type.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/J/Type.thy Thu Feb 11 08:44:41 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/J/Type.thy
- ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
*)
@@ -47,12 +46,10 @@
= PrimT prim_ty -- "primitive type"
| RefT ref_ty -- "reference type"
-syntax
- NT :: "ty"
- Class :: "cname => ty"
+abbreviation NT :: ty
+ where "NT == RefT NullT"
-translations
- "NT" == "RefT NullT"
- "Class C" == "RefT (ClassT C)"
+abbreviation Class :: "cname => ty"
+ where "Class C == RefT (ClassT C)"
end
--- a/src/HOL/MicroJava/J/WellType.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Thu Feb 11 08:44:41 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/J/WellType.thy
- ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
*)
@@ -27,13 +26,13 @@
lenv = "vname \<rightharpoonup> ty"
'c env = "'c prog \<times> lenv"
-syntax
- prg :: "'c env => 'c prog"
- localT :: "'c env => (vname \<rightharpoonup> ty)"
+abbreviation (input)
+ prg :: "'c env => 'c prog"
+ where "prg == fst"
-translations
- "prg" => "fst"
- "localT" => "snd"
+abbreviation (input)
+ localT :: "'c env => (vname \<rightharpoonup> ty)"
+ where "localT == snd"
consts
more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
@@ -207,10 +206,7 @@
(let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
-syntax
- wf_java_prog :: "'c prog => bool"
-translations
- "wf_java_prog" == "wf_prog wf_java_mdecl"
+abbreviation "wf_java_prog == wf_prog wf_java_mdecl"
lemma wf_java_prog_wf_java_mdecl: "\<lbrakk>
wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths \<rbrakk>
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Thu Feb 11 08:44:41 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/JVM/JVMDefensive.thy
- ID: $Id$
Author: Gerwin Klein
*)
@@ -13,9 +12,9 @@
datatype 'a type_error = TypeError | Normal 'a
-syntax "fifth" :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e"
-translations
- "fifth x" == "fst(snd(snd(snd(snd x))))"
+abbreviation
+ fifth :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e"
+ where "fifth x == fst(snd(snd(snd(snd x))))"
consts isAddr :: "val \<Rightarrow> bool"
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Thu Feb 11 08:44:41 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/JVM/JVMExceptions.thy
- ID: $Id$
Author: Gerwin Klein, Martin Strecker
Copyright 2001 Technische Universitaet Muenchen
*)
@@ -24,10 +23,9 @@
then Some (fst (snd (snd e)))
else match_exception_table G cn pc es)"
-consts
+abbreviation
ex_table_of :: "jvm_method \<Rightarrow> exception_table"
-translations
- "ex_table_of m" == "snd (snd (snd m))"
+ where "ex_table_of m == snd (snd (snd m))"
consts
--- a/src/HOL/NanoJava/Example.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/NanoJava/Example.thy Thu Feb 11 08:44:41 2010 +0100
@@ -50,11 +50,14 @@
consts suc :: mname
add :: mname
consts any :: vname
-syntax dummy:: expr ("<>")
- one :: expr
-translations
- "<>" == "LAcc any"
- "one" == "{Nat}new Nat..suc(<>)"
+
+abbreviation
+ dummy :: expr ("<>")
+ where "<> == LAcc any"
+
+abbreviation
+ one :: expr
+ where "one == {Nat}new Nat..suc(<>)"
text {* The following properties could be derived from a more complete
program model, which we leave out for laziness. *}
--- a/src/HOL/NanoJava/TypeRel.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Thu Feb 11 08:44:41 2010 +0100
@@ -11,16 +11,16 @@
consts
subcls1 :: "(cname \<times> cname) set" --{* subclass *}
-syntax (xsymbols)
- subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _" [71,71] 70)
- subcls :: "[cname, cname] => bool" ("_ \<preceq>C _" [71,71] 70)
-syntax
- subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
- subcls :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70)
+abbreviation
+ subcls1_syntax :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
+ where "C <=C1 D == (C,D) \<in> subcls1"
+abbreviation
+ subcls_syntax :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70)
+ where "C <=C D == (C,D) \<in> subcls1^*"
-translations
- "C \<prec>C1 D" == "(C,D) \<in> subcls1"
- "C \<preceq>C D" == "(C,D) \<in> subcls1^*"
+notation (xsymbols)
+ subcls1_syntax ("_ \<prec>C1 _" [71,71] 70) and
+ subcls_syntax ("_ \<preceq>C _" [71,71] 70)
consts
method :: "cname => (mname \<rightharpoonup> methd)"
--- a/src/HOL/SET_Protocol/Event_SET.thy Thu Feb 11 08:44:19 2010 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy Thu Feb 11 08:44:41 2010 +0100
@@ -11,8 +11,7 @@
begin
text{*The Root Certification Authority*}
-syntax RCA :: agent
-translations "RCA" == "CA 0"
+abbreviation "RCA == CA 0"
text{*Message events*}