--- a/src/HOL/Bali/Conform.thy Mon Apr 26 14:54:45 2004 +0200
+++ b/src/HOL/Bali/Conform.thy Mon Apr 26 14:56:18 2004 +0200
@@ -26,7 +26,7 @@
constdefs
- gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_" [71,71] 70)
+ gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_" [71,71] 70)
"s\<le>|s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj"
text {* For the the proof of type soundness we will need the
@@ -186,7 +186,7 @@
constdefs
lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
- ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
+ ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
"G,s\<turnstile>vs[\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
lemma lconfD: "\<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T"
@@ -272,7 +272,7 @@
constdefs
wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
- ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
+ ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
"G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
lemma wlconfD: "\<lbrakk>G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts; Ts n = Some T; vs n = Some v\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
@@ -389,7 +389,7 @@
constdefs
- conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool" ( "_\<Colon>\<preceq>_" [71,71] 70)
+ conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool" ( "_\<Colon>\<preceq>_" [71,71] 70)
"xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
(\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and>
\<spacespace> G,s\<turnstile>l [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
--- a/src/HOL/Bali/Decl.thy Mon Apr 26 14:54:45 2004 +0200
+++ b/src/HOL/Bali/Decl.thy Mon Apr 26 14:56:18 2004 +0200
@@ -366,9 +366,9 @@
consts
- Object_mdecls :: "mdecl list" --{* methods of Object *}
- SXcpt_mdecls :: "mdecl list" --{* methods of SXcpts *}
- ObjectC :: "cdecl" --{* declaration of root class *}
+ Object_mdecls :: "mdecl list" --{* methods of Object *}
+ SXcpt_mdecls :: "mdecl list" --{* methods of SXcpts *}
+ ObjectC :: "cdecl" --{* declaration of root class *}
SXcptC ::"xname \<Rightarrow> cdecl" --{* declarations of throwable classes *}
defs
--- a/src/HOL/Bali/Evaln.thy Mon Apr 26 14:54:45 2004 +0200
+++ b/src/HOL/Bali/Evaln.thy Mon Apr 26 14:56:18 2004 +0200
@@ -57,7 +57,7 @@
evalsn:: "[prog, state, expr list, val list, nat, state] \<Rightarrow> bool"
("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
execn :: "[prog, state, stmt , nat, state] \<Rightarrow> bool"
- ("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _" [61,61,65, 61,61] 60)
+ ("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _" [61,61,65, 61,61] 60)
translations
--- a/src/HOL/Bali/TypeRel.thy Mon Apr 26 14:54:45 2004 +0200
+++ b/src/HOL/Bali/TypeRel.thy Mon Apr 26 14:56:18 2004 +0200
@@ -29,16 +29,16 @@
consts
-(*subint1, in Decl.thy*) (* direct subinterface *)
-(*subint , by translation*) (* subinterface (+ identity) *)
-(*subcls1, in Decl.thy*) (* direct subclass *)
-(*subcls , by translation*) (* subclass *)
-(*subclseq, by translation*) (* subclass + identity *)
+(*subint1, in Decl.thy*) (* direct subinterface *)
+(*subint , by translation*) (* subinterface (+ identity) *)
+(*subcls1, in Decl.thy*) (* direct subclass *)
+(*subcls , by translation*) (* subclass *)
+(*subclseq, by translation*) (* subclass + identity *)
implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
- implmt :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* implementation *}
+ implmt :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* implementation *}
widen :: "prog \<Rightarrow> (ty \<times> ty ) set" --{* widening *}
narrow :: "prog \<Rightarrow> (ty \<times> ty ) set" --{* narrowing *}
- cast :: "prog \<Rightarrow> (ty \<times> ty ) set" --{* casting *}
+ cast :: "prog \<Rightarrow> (ty \<times> ty ) set" --{* casting *}
syntax