# HG changeset patch
# User kleing
# Date 969632933 -7200
# Node ID fe82134773dc86f967ad88c83a99792a2318a0d0
# Parent  4522e59b7d8466460d77bd4375d39deae010ce32
added HTML syntax; added spaces in normal syntax for better documents

diff -r 4522e59b7d84 -r fe82134773dc src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Fri Sep 22 16:28:53 2000 +0200
@@ -12,23 +12,43 @@
 
 constdefs
 
-  hext :: "aheap => aheap => bool"		 (     "_\\<le>|_"  [51,51] 50)
+  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'))"
 
-  conf :: "'c prog => aheap => val => ty => bool"	 ( "_,_\\<turnstile>_::\\<preceq>_"  [51,51,51,51] 50)
+  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"
 
   lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
-                                                 ("_,_\\<turnstile>_[::\\<preceq>]_" [51,51,51,51] 50)
+                                                ("_,_ \\<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)"
 
-  oconf :: "'c prog => aheap => obj => bool"      ("_,_\\<turnstile>_\\<surd>"     [51,51,51]    50)
+  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))"
 
-  hconf :: "'c prog => aheap => bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
+  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>"
 
-  conforms :: "state => java_mb env_ => bool"	 ("_::\\<preceq>_"       [51,51]       50)
+  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"
 
+
+syntax (HTML)
+  hext     :: "aheap => aheap => bool"
+              ("_ <=| _" [51,51] 50)
+
+  conf     :: "'c prog => aheap => val => ty => bool"
+              ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
+
+  lconf    :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
+              ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
+
+  oconf    :: "'c prog => aheap => obj => bool"
+              ("_,_ |- _ [ok]" [51,51,51] 50)
+
+  hconf    :: "'c prog => aheap => bool"
+              ("_ |-h _ [ok]" [51,51] 50)
+
+  conforms :: "state => java_mb env_ => bool"
+              ("_ ::<= _" [51,51] 50)
+
 end
diff -r 4522e59b7d84 -r fe82134773dc src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Fri Sep 22 16:28:53 2000 +0200
@@ -16,12 +16,22 @@
 
 syntax
   eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
-          ("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
+          ("_ \\<turnstile> _ -_\\<succ>_-> _" [51,82,82,82,82] 81)
   evals:: "[java_mb prog,xstate,expr list,
                         val list,xstate] => bool "
-          ("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
+          ("_ \\<turnstile> _ -_[\\<succ>]_-> _" [51,82,51,51,82] 81)
   exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
-          ("_\\<turnstile>_ -_-> _"  [51,82,82,   82]81)
+          ("_ \\<turnstile> _ -_-> _" [51,82,82,82] 81)
+
+syntax (HTML)
+  eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
+          ("_ |- _ -_>_-> _" [51,82,82,82,82] 81)
+  evals:: "[java_mb prog,xstate,expr list,
+                        val list,xstate] => bool "
+          ("_ |- _ -_[>]_-> _" [51,82,51,51,82] 81)
+  exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
+          ("_ |- _ -_-> _" [51,82,82,82] 81)
+
 
 translations
   "G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval  G"
diff -r 4522e59b7d84 -r fe82134773dc src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Fri Sep 22 16:28:53 2000 +0200
@@ -14,7 +14,6 @@
         obj = "cname \\<times> fields_"	(* class instance with class name and fields *)
 
 constdefs
-
   obj_ty	:: "obj => ty"
  "obj_ty obj  == Class (fst obj)"
 
@@ -42,9 +41,9 @@
   Norm		:: "state => xstate"
 
 translations
-  "heap"	=> "fst"
-  "locals"	=> "snd"
-  "Norm s"      == "(None,s)"  
+  "heap"   => "fst"
+  "locals" => "snd"
+  "Norm s" == "(None,s)"  
 
 constdefs
 
diff -r 4522e59b7d84 -r fe82134773dc src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Fri Sep 22 16:28:53 2000 +0200
@@ -11,21 +11,23 @@
 datatype binop = Eq | Add	   (* function codes for binary operation *)
 
 datatype expr
-	= NewC	cname		   (* class instance creation *)
-	| Cast	cname expr	   (* type cast *)
-	| Lit	val		   (* literal value, also references *)
-        | BinOp binop  expr expr   (* binary operation *)
-	| LAcc vname		   (* local (incl. parameter) access *)
-	| LAss vname expr          (* local assign *) ("_::=_"  [      90,90]90)
-	| FAcc cname expr vname    (* field access *) ("{_}_.._"[10,90,99   ]90)
+	= NewC	cname              (* class instance creation *)
+	| Cast	cname expr         (* type cast *)
+	| Lit	val                  (* literal value, also references *)
+  | BinOp binop  expr expr   (* binary operation *)
+	| LAcc vname               (* local (incl. parameter) access *)
+	| LAss vname expr          (* local assign *) ("_::=_"   [      90,90]90)
+	| FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
 	| FAss cname expr vname 
-	                  expr     (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
-	| Call expr mname (ty list) (expr list)(* method call*)
-                                    ("_.._'({_}_')" [90,99,10,10] 90)
+                    expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
+	| Call expr mname 
+    (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
+
 and stmt
-	= Skip			   (* empty      statement *)
-	| Expr expr		   (* expression statement *)
-	| Comp stmt stmt	   ("_;; _"			[      61,60]60)
-	| Cond expr stmt stmt      ("If'(_') _ Else _"		[   80,79,79]70)
-	| Loop expr stmt	   ("While'(_') _"		[      80,79]70)
+	= Skip                     (* empty statement *)
+  | Expr expr                (* expression statement *)
+  | Comp stmt stmt       ("_;; _"             [61,60]60)
+  | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
+  | Loop expr stmt       ("While '(_') _"     [80,79]70)
+
 end
diff -r 4522e59b7d84 -r fe82134773dc src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Type.thy	Fri Sep 22 16:28:53 2000 +0200
@@ -8,32 +8,35 @@
 
 Type = JBasis +
 
-types	cname		(* class name *)
-        vnam		(* variable or field name *)
-	mname		(* method name *)
+types cname   (* class name *)
+      vnam    (* variable or field name *)
+      mname   (* method name *)
+
 arities cname, vnam, mname :: term
 
 datatype vname		(* names for This pointer and local/field variables *)
-	= This
-	| VName   vnam
+  = This
+  | VName vnam
 
-datatype prim_ty       	(* primitive type, cf. 4.2 *)
-	= Void    	(* 'result type' of void methods *)
-	| Boolean
-	| Integer
+datatype prim_ty  (* primitive type, cf. 4.2 *)
+  = Void          (* 'result type' of void methods *)
+  | Boolean
+  | Integer
 
 datatype ref_ty		(* reference type, cf. 4.3 *)
-	= NullT		(* null type, cf. 4.1 *)
-	| ClassT cname	(* class type *)
-datatype ty    		(* any type, cf. 4.1 *)
-	= PrimT prim_ty	(* primitive type *)
-	| RefT  ref_ty	(* reference type *)
+  = NullT		      (* null type, cf. 4.1 *)
+  | ClassT cname  (* class type *)
+
+datatype ty       (* any type, cf. 4.1 *)
+  = PrimT prim_ty (* primitive type *)
+  | RefT  ref_ty  (* reference type *)
 
 syntax
-         NT     :: "          ty"
-	 Class	:: "cname  => ty"
+  NT    :: "          ty"
+	Class	:: "cname  => ty"
+
 translations
-	"NT"      == "RefT   NullT"
+	"NT"      == "RefT NullT"
 	"Class C" == "RefT (ClassT C)"
 
 end
diff -r 4522e59b7d84 -r fe82134773dc src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Sep 22 16:28:53 2000 +0200
@@ -9,21 +9,27 @@
 TypeRel = Decl +
 
 consts
-  subcls1	:: "'c prog => (cname \\<times> cname) set"  (* subclass *)
-  widen 	:: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
-  cast		:: "'c prog => (cname \\<times> cname) set"  (* casting *)
+  subcls1 :: "'c prog => (cname \\<times> cname) set"  (* subclass *)
+  widen   :: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
+  cast    :: "'c prog => (cname \\<times> cname) set"  (* casting *)
 
 syntax
-  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)
+  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)
+
+syntax (HTML)
+  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)
 
 translations
-  	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
-	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
-	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
-	"G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
+  "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
+  "G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
+  "G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
+  "G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
 
 defs
 
diff -r 4522e59b7d84 -r fe82134773dc src/HOL/MicroJava/J/Value.thy
--- a/src/HOL/MicroJava/J/Value.thy	Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Value.thy	Fri Sep 22 16:28:53 2000 +0200
@@ -8,44 +8,45 @@
 
 Value = Type +
 
-types   loc		(* locations, i.e. abstract references on objects *)
+types   loc     (* locations, i.e. abstract references on objects *)
 arities loc :: term
 
-datatype val_		(* name non 'val' because of clash with ML token *)
-	= Unit		(* dummy result value of void methods *)
-	| Null		(* null reference *)
-	| Bool bool	(* Boolean value *)
-	| Intg int	(* integer value *) (* Name Intg instead of Int because
-					       of clash with HOL/Set.thy *)
-	| Addr loc	(* addresses, i.e. locations of objects *)
+datatype val_   (* name non 'val' because of clash with ML token *)
+  = Unit        (* dummy result value of void methods *)
+  | Null        (* null reference *)
+  | Bool bool   (* Boolean value *)
+  | Intg int    (* integer value, name Intg instead of Int because
+                   of clash with HOL/Set.thy *)
+  | Addr loc    (* addresses, i.e. locations of objects *)
+
 types	val = val_
 translations "val" <= (type) "val_"
 
 consts
-  the_Bool	:: "val => bool"
-  the_Intg	:: "val => int"
-  the_Addr	:: "val => loc"
+  the_Bool :: "val => bool"
+  the_Intg :: "val => int"
+  the_Addr :: "val => loc"
 
 primrec
- "the_Bool (Bool b) = b"
+  "the_Bool (Bool b) = b"
 
 primrec
- "the_Intg (Intg i) = i"
+  "the_Intg (Intg i) = i"
 
 primrec
- "the_Addr (Addr a) = a"
+  "the_Addr (Addr a) = a"
 
 consts
-  defpval	:: "prim_ty => val"	(* default value for primitive types *)
-  default_val	:: "ty => val"		(* default value for all types *)
+  defpval :: "prim_ty => val"  (* default value for primitive types *)
+  default_val :: "ty => val"   (* default value for all types *)
 
 primrec
-	"defpval Void    = Unit"
-	"defpval Boolean = Bool False"
-	"defpval Integer = Intg (#0)"
+  "defpval Void    = Unit"
+  "defpval Boolean = Bool False"
+  "defpval Integer = Intg (#0)"
 
 primrec
-	"default_val (PrimT pt) = defpval pt"
-	"default_val (RefT  r ) = Null"
+  "default_val (PrimT pt) = defpval pt"
+  "default_val (RefT  r ) = Null"
 
 end
diff -r 4522e59b7d84 -r fe82134773dc src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Fri Sep 22 16:28:53 2000 +0200
@@ -19,17 +19,16 @@
 types 'c wf_mb = 'c prog => cname => 'c mdecl => bool
 
 constdefs
-
- wf_fdecl	:: "'c prog =>          fdecl => bool"
+ wf_fdecl	:: "'c prog => fdecl => bool"
 "wf_fdecl G == \\<lambda>(fn,ft). is_type G ft"
 
- wf_mhead	:: "'c prog => sig   => ty => bool"
+ wf_mhead	:: "'c prog => sig => ty => bool"
 "wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
 
- wf_mdecl	:: "'c wf_mb => 'c wf_mb"
+ wf_mdecl :: "'c wf_mb => 'c wf_mb"
 "wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
 
-  wf_cdecl	:: "'c wf_mb => 'c prog => 'c cdecl => bool"
+ wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
 "wf_cdecl wf_mb G ==
    \\<lambda>(C,(sc,fs,ms)).
 	(\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
@@ -40,7 +39,7 @@
              (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
                  method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
 
- wf_prog	:: "'c wf_mb => 'c prog => bool"
+ wf_prog :: "'c wf_mb => 'c prog => bool"
 "wf_prog wf_mb G ==
    let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
 
diff -r 4522e59b7d84 -r fe82134773dc src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Fri Sep 22 16:28:53 2000 +0200
@@ -23,26 +23,22 @@
 	= "'c prog \\<times> lenv"
 
 syntax
-
-  prg		:: "'c env => 'c prog"
-  localT	:: "'c env => (vname \\<leadsto> ty)"
+  prg    :: "'c env => 'c prog"
+  localT :: "'c env => (vname \\<leadsto> ty)"
 
 translations	
-
-  "prg"		=> "fst"
-  "localT"	=> "snd"
+  "prg"    => "fst"
+  "localT" => "snd"
 
 consts
-
-  more_spec	:: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
-		               (ty \\<times> 'x) \\<times> ty list => bool"
-  appl_methds	:: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
-  max_spec	:: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
+  more_spec :: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
+                (ty \\<times> 'x) \\<times> ty list => bool"
+  appl_methds :: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
+  max_spec :: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
 
 defs
-
-  more_spec_def	  "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
-		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
+  more_spec_def "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
+		                            list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
   
   (* applicable methods, cf. 15.11.2.1 *)
   appl_methds_def "appl_methds G C == \\<lambda>(mn, pTs).
@@ -51,11 +47,11 @@
 		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
 
   (* maximally specific methods, cf. 15.11.2.2 *)
-   max_spec_def	  "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and> 
-				          (\\<forall>m'\\<in>appl_methds G C sig.
-				                   more_spec G m' m --> m' = m)}"
+  max_spec_def "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and> 
+                                      (\\<forall>m'\\<in>appl_methds G C sig.
+                                        more_spec G m' m --> m' = m)}"
+
 consts
-
   typeof :: "(loc => ty option) => val => ty option"
 
 primrec
@@ -70,16 +66,20 @@
 	(* method body with parameter names, local variables, block, result expression *)
 
 consts
-
   ty_expr :: "java_mb env => (expr      \\<times> ty     ) set"
   ty_exprs:: "java_mb env => (expr list \\<times> ty list) set"
   wt_stmt :: "java_mb env =>  stmt                 set"
 
 syntax
+  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)
 
-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)
+  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)
+
 
 translations
 	"E\\<turnstile>e :: T" == "(e,T) \\<in> ty_expr  E"
@@ -91,84 +91,84 @@
 (* well-typed expressions *)
 
   (* cf. 15.8 *)
-  NewC	"[|is_class (prg E) C|] ==>
-						 E\\<turnstile>NewC C::Class C"
+  NewC	"[| is_class (prg E) C |] ==>
+         E\\<turnstile>NewC C::Class C"
 
   (* cf. 15.15 *)
-  Cast	"[|E\\<turnstile>e::Class C;
-	  prg E\\<turnstile>C\\<preceq>? D|] ==>
-						 E\\<turnstile>Cast D e::Class D"
+  Cast  "[| E\\<turnstile>e::Class C;
+            prg E\\<turnstile>C\\<preceq>? D |] ==>
+         E\\<turnstile>Cast D e::Class D"
 
   (* cf. 15.7.1 *)
-  Lit	"[|typeof (\\<lambda>v. None) x = Some T|] ==>
-						 E\\<turnstile>Lit x::T"
+  Lit	  "[| typeof (\\<lambda>v. None) x = Some T |] ==>
+         E\\<turnstile>Lit x::T"
 
   
   (* cf. 15.13.1 *)
-  LAcc	"[|localT E v = Some T; is_type (prg E) T|] ==>
-						 E\\<turnstile>LAcc v::T"
+  LAcc  "[| localT E v = Some T; is_type (prg E) T |] ==>
+         E\\<turnstile>LAcc v::T"
 
-  BinOp "[|E\\<turnstile>e1::T;
-	  E\\<turnstile>e2::T;
-	  if bop = Eq then T' = PrimT Boolean
-	              else T' = T \\<and> T = PrimT Integer|] ==>
-						 E\\<turnstile>BinOp bop e1 e2::T'"
+  BinOp "[| E\\<turnstile>e1::T;
+            E\\<turnstile>e2::T;
+            if bop = Eq then T' = PrimT Boolean
+                        else T' = T \\<and> T = PrimT Integer|] ==>
+         E\\<turnstile>BinOp bop e1 e2::T'"
 
   (* cf. 15.25, 15.25.1 *)
-  LAss  "[|E\\<turnstile>LAcc v::T;
-	  E\\<turnstile>e::T';
-	  prg E\\<turnstile>T'\\<preceq>T|] ==>
-						 E\\<turnstile>v::=e::T'"
+  LAss  "[| E\\<turnstile>LAcc v::T;
+	          E\\<turnstile>e::T';
+            prg E\\<turnstile>T'\\<preceq>T |] ==>
+         E\\<turnstile>v::=e::T'"
 
   (* cf. 15.10.1 *)
-  FAcc	"[|E\\<turnstile>a::Class C; 
-	  field (prg E,C) fn = Some (fd,fT)|] ==>
-						 E\\<turnstile>{fd}a..fn::fT"
+  FAcc  "[| E\\<turnstile>a::Class C; 
+            field (prg E,C) fn = Some (fd,fT) |] ==>
+         E\\<turnstile>{fd}a..fn::fT"
 
   (* cf. 15.25, 15.25.1 *)
-  FAss  "[|E\\<turnstile>{fd}a..fn::T;
-	  E\\<turnstile>v       ::T';
-	  prg E\\<turnstile>T'\\<preceq>T|] ==>
-					 	 E\\<turnstile>{fd}a..fn:=v::T'"
+  FAss  "[| E\\<turnstile>{fd}a..fn::T;
+            E\\<turnstile>v        ::T';
+            prg E\\<turnstile>T'\\<preceq>T |] ==>
+         E\\<turnstile>{fd}a..fn:=v::T'"
 
 
   (* cf. 15.11.1, 15.11.2, 15.11.3 *)
-  Call	"[|E\\<turnstile>a::Class C;
-	  E\\<turnstile>ps[::]pTs;
-	  max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}|] ==>
-						 E\\<turnstile>a..mn({pTs'}ps)::rT"
+  Call  "[| E\\<turnstile>a::Class C;
+            E\\<turnstile>ps[::]pTs;
+            max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
+         E\\<turnstile>a..mn({pTs'}ps)::rT"
 
 (* well-typed expression lists *)
 
   (* cf. 15.11.??? *)
-  Nil						"E\\<turnstile>[][::][]"
+  Nil  "E\\<turnstile>[][::][]"
 
   (* cf. 15.11.??? *)
-  Cons	"[|E\\<turnstile>e::T;
-	   E\\<turnstile>es[::]Ts|] ==>
-						 E\\<turnstile>e#es[::]T#Ts"
+  Cons "[| E\\<turnstile>e::T;
+           E\\<turnstile>es[::]Ts |] ==>
+        E\\<turnstile>e#es[::]T#Ts"
 
 (* well-typed statements *)
 
-  Skip					"E\\<turnstile>Skip\\<surd>"
+  Skip "E\\<turnstile>Skip\\<surd>"
 
-  Expr	"[|E\\<turnstile>e::T|] ==>
-					 E\\<turnstile>Expr e\\<surd>"
+  Expr "[| E\\<turnstile>e::T |] ==>
+        E\\<turnstile>Expr e\\<surd>"
 
-  Comp	"[|E\\<turnstile>s1\\<surd>; 
-	  E\\<turnstile>s2\\<surd>|] ==>
-					 E\\<turnstile>s1;; s2\\<surd>"
+  Comp "[| E\\<turnstile>s1\\<surd>; 
+           E\\<turnstile>s2\\<surd> |] ==>
+        E\\<turnstile>s1;; s2\\<surd>"
 
   (* cf. 14.8 *)
-  Cond	"[|E\\<turnstile>e::PrimT Boolean;
-	  E\\<turnstile>s1\\<surd>;
-	  E\\<turnstile>s2\\<surd>|] ==>
-					 E\\<turnstile>If(e) s1 Else s2\\<surd>"
+  Cond "[| E\\<turnstile>e::PrimT Boolean;
+           E\\<turnstile>s1\\<surd>;
+           E\\<turnstile>s2\\<surd> |] ==>
+         E\\<turnstile>If(e) s1 Else s2\\<surd>"
 
   (* cf. 14.10 *)
-  Loop "[|E\\<turnstile>e::PrimT Boolean;
-	 E\\<turnstile>s\\<surd>|] ==>
-					 E\\<turnstile>While(e) s\\<surd>"
+  Loop "[| E\\<turnstile>e::PrimT Boolean;
+           E\\<turnstile>s\\<surd> |] ==>
+        E\\<turnstile>While(e) s\\<surd>"
 
 constdefs