# HG changeset patch
# User oheimb
# Date 992347860 -7200
# Node ID 648795477bb5f6c4a08f407da408bf7df7305f5b
# Parent  1d5d181b7e2876af4c246f7bfa84480c34c8c551
corrected xsymbol/HTML syntax

diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -56,7 +56,7 @@
 
 constdefs
  correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
-                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
+                  ("_,_ |-JVM _ [ok]"  [51,51] 50)
 "correct_state G phi == \<lambda>(xp,hp,frs).
    case xp of
      None => (case frs of
@@ -73,9 +73,9 @@
    | Some x => True" 
 
 
-syntax (HTML)
+syntax (xsymbols)
  correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
-                  ("_,_ |-JVM _ [ok]"  [51,51] 50)
+                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
 
 
 lemma sup_ty_opt_OK:
diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -43,31 +43,31 @@
 
 constdefs
   sup_ty_opt :: "['code prog,ty err,ty err] => bool" 
-                 ("_ \<turnstile> _ <=o _" [71,71] 70)
+                 ("_ |- _ <=o _" [71,71] 70)
   "sup_ty_opt G == Err.le (subtype G)"
 
   sup_loc :: "['code prog,locvars_type,locvars_type] => bool" 
-              ("_ \<turnstile> _ <=l _"  [71,71] 70)
+              ("_ |- _ <=l _"  [71,71] 70)
   "sup_loc G == Listn.le (sup_ty_opt G)"
 
   sup_state :: "['code prog,state_type,state_type] => bool"	  
-               ("_ \<turnstile> _ <=s _"  [71,71] 70)
+               ("_ |- _ <=s _"  [71,71] 70)
   "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
 
   sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
-                   ("_ \<turnstile> _ <=' _"  [71,71] 70)
+                   ("_ |- _ <=' _"  [71,71] 70)
   "sup_state_opt G == Opt.le (sup_state G)"
 
 
-syntax (HTML) 
+syntax (xsymbols)
   sup_ty_opt    :: "['code prog,ty err,ty err] => bool" 
-                   ("_ |- _ <=o _")
+                   ("_ \<turnstile> _ <=o _" [71,71] 70)
   sup_loc       :: "['code prog,locvars_type,locvars_type] => bool" 
-                   ("_ |- _ <=l _"  [71,71] 70)
+                   ("_ \<turnstile> _ <=l _" [71,71] 70)
   sup_state     :: "['code prog,state_type,state_type] => bool"	
-                   ("_ |- _ <=s _"  [71,71] 70)
+                   ("_ \<turnstile> _ <=s _" [71,71] 70)
   sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
-                   ("_ |- _ <=' _"  [71,71] 70)
+                   ("_ \<turnstile> _ <=' _" [71,71] 70)
                    
 
 lemma JVM_states_unfold: 
diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -12,44 +12,45 @@
 
 constdefs
 
-  hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50)
- "h\<le>|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
+  hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50)
+ "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
 
-  conf :: "'c prog => aheap => val => ty => bool"	("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
- "G,h\<turnstile>v::\<preceq>T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
+  conf :: "'c prog => aheap => val => ty => bool"	
+                                   ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
+ "G,h|-v::<=T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
 
   lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
-                                                ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
- "G,h\<turnstile>vs[::\<preceq>]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h\<turnstile>v::\<preceq>T)"
+                                   ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
+ "G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)"
 
-  oconf :: "'c prog => aheap => obj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
- "G,h\<turnstile>obj\<surd> == G,h\<turnstile>snd obj[::\<preceq>]map_of (fields (G,fst obj))"
+  oconf :: "'c prog => aheap => obj => bool" ("_,_ |- _ [ok]" [51,51,51] 50)
+ "G,h|-obj [ok] == G,h|-snd obj[::<=]map_of (fields (G,fst obj))"
 
-  hconf :: "'c prog => aheap => bool" ("_ \<turnstile>h _ \<surd>" [51,51] 50)
- "G\<turnstile>h h\<surd>    == \<forall>a obj. h a = Some obj --> G,h\<turnstile>obj\<surd>"
+  hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50)
+ "G|-h h [ok]    == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]"
 
-  conforms :: "state => java_mb env_ => bool"	("_ ::\<preceq> _" [51,51] 50)
- "s::\<preceq>E == prg E\<turnstile>h heap s\<surd> \<and> prg E,heap s\<turnstile>locals s[::\<preceq>]localT E"
+  conforms :: "state => java_mb env_ => bool"	("_ ::<= _" [51,51] 50)
+ "s::<=E == prg E|-h heap s [ok] \<and> prg E,heap s|-locals s[::<=]localT E"
 
 
-syntax (HTML)
+syntax (xsymbols)
   hext     :: "aheap => aheap => bool"
-              ("_ <=| _" [51,51] 50)
+              ("_ \<le>| _" [51,51] 50)
 
   conf     :: "'c prog => aheap => val => ty => bool"
-              ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
+              ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
 
   lconf    :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
-              ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
+              ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
 
   oconf    :: "'c prog => aheap => obj => bool"
-              ("_,_ |- _ [ok]" [51,51,51] 50)
+              ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
 
   hconf    :: "'c prog => aheap => bool"
-              ("_ |-h _ [ok]" [51,51] 50)
+              ("_ \<turnstile>h _ \<surd>" [51,51] 50)
 
   conforms :: "state => java_mb env_ => bool"
-              ("_ ::<= _" [51,51] 50)
+              ("_ ::\<preceq> _" [51,51] 50)
 
 
 section "hext"
diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/MicroJava/J/Decl.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    Copyright   1999 Technische Universitaet Muenchen
 *)
 
 header "Class Declarations and whole Programs"
diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -13,7 +13,7 @@
   evals :: "java_mb prog => (xstate \<times> expr list \<times> val list \<times> xstate) set"
   exec  :: "java_mb prog => (xstate \<times> stmt                 \<times> xstate) set"
 
-syntax
+syntax (xsymbols)
   eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
           ("_ \<turnstile> _ -_\<succ>_-> _" [51,82,60,82,82] 81)
   evals:: "[java_mb prog,xstate,expr list,
@@ -22,7 +22,7 @@
   exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
           ("_ \<turnstile> _ -_-> _" [51,82,60,82] 81)
 
-syntax (HTML)
+syntax
   eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
           ("_ |- _ -_>_-> _" [51,82,60,82,82] 81)
   evals:: "[java_mb prog,xstate,expr list,
diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -1,7 +1,7 @@
 (*  Title:      isabelle/Bali/Example.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    Copyright   1999 Technische Universitaet Muenchen
 *)
 
 header "Example MicroJava Program"
diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -25,7 +25,7 @@
 	| ClassCast
 	| OutOfMemory
 
-types	aheap  = "loc \<leadsto> obj" (* "heap" used in a translation below *)
+types	aheap  = "loc \<leadsto> obj" (** "heap" used in a translation below **)
         locals = "vname \<leadsto> val"	
 
         state		(* simple state, i.e. variable contents *)
diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -13,17 +13,17 @@
   widen   :: "'c prog => (ty    \<times> ty   ) set"  (* widening *)
   cast    :: "'c prog => (cname \<times> cname) set"  (* casting *)
 
-syntax
+syntax (xsymbols)
   subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
-  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
-  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
-  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
+  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _"  [71,71,71] 70)
+  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
+  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
 
-syntax (HTML)
+syntax
   subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
-  subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
-  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _" [71,71,71] 70)
-  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
+  subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _"  [71,71,71] 70)
+  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _"   [71,71,71] 70)
+  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _"  [71,71,71] 70)
 
 translations
   "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -103,12 +103,12 @@
   ty_exprs:: "java_mb env => (expr list \<times> ty list) set"
   wt_stmt :: "java_mb env =>  stmt                 set"
 
-syntax
+syntax (xsymbols)
   ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ \<turnstile> _ :: _"   [51,51,51]50)
   ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
   wt_stmt :: "java_mb env =>  stmt                => bool" ("_ \<turnstile> _ \<surd>"      [51,51   ]50)
 
-syntax (HTML)
+syntax
   ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ |- _ :: _"   [51,51,51]50)
   ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
   wt_stmt :: "java_mb env =>  stmt                => bool" ("_ |- _ [ok]"   [51,51   ]50)
diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -28,12 +28,12 @@
 
 constdefs
   exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  
-              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
-  "G \<turnstile> s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
+              ("_ |- _ -jvm-> _" [61,61,61]60)
+  "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
 
 
-syntax (HTML)
+syntax (xsymbols)
   exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  
-              ("_ |- _ -jvm-> _" [61,61,61]60)
+              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
 
 end