# HG changeset patch
# User wenzelm
# Date 1082984178 -7200
# Node ID 3506a9af46fc85577a7af7eb677e66f51d26ab44
# Parent  3d760a971fde80cdd81f736acedcf1072cc08d6b
*** empty log message ***

diff -r 3d760a971fde -r 3506a9af46fc src/HOL/Bali/Conform.thy
--- 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>
diff -r 3d760a971fde -r 3506a9af46fc src/HOL/Bali/Decl.thy
--- 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 
diff -r 3d760a971fde -r 3506a9af46fc src/HOL/Bali/Evaln.thy
--- 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
 
diff -r 3d760a971fde -r 3506a9af46fc src/HOL/Bali/TypeRel.thy
--- 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