# HG changeset patch
# User kleing
# Date 969876529 -7200
# Node ID c7226e6f9625236e14e189fca538138c9595d793
# Parent  46db6fde4ee3009b021537723cf8ddf6c0f868a2
untabified for HTML

diff -r 46db6fde4ee3 -r c7226e6f9625 src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Mon Sep 25 12:04:10 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Mon Sep 25 12:08:49 2000 +0200
@@ -8,23 +8,23 @@
 
 Term = Value + 
 
-datatype binop = Eq | Add	   (* function codes for binary operation *)
+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)
-	| FAss cname expr vname 
+  = 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 
+  | Call expr mname 
     (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
 
 and stmt
-	= Skip                     (* empty statement *)
+  = Skip                     (* empty statement *)
   | Expr expr                (* expression statement *)
   | Comp stmt stmt       ("_;; _"             [61,60]60)
   | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
diff -r 46db6fde4ee3 -r c7226e6f9625 src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Mon Sep 25 12:04:10 2000 +0200
+++ b/src/HOL/MicroJava/J/Type.thy	Mon Sep 25 12:08:49 2000 +0200
@@ -14,7 +14,7 @@
 
 arities cname, vnam, mname :: term
 
-datatype vname		(* names for This pointer and local/field variables *)
+datatype vname    (* names for This pointer and local/field variables *)
   = This
   | VName vnam
 
@@ -23,8 +23,8 @@
   | Boolean
   | Integer
 
-datatype ref_ty		(* reference type, cf. 4.3 *)
-  = NullT		      (* null type, cf. 4.1 *)
+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 *)
@@ -33,10 +33,10 @@
 
 syntax
   NT    :: "          ty"
-	Class	:: "cname  => ty"
+  Class :: "cname  => ty"
 
 translations
-	"NT"      == "RefT NullT"
-	"Class C" == "RefT (ClassT C)"
+  "NT"      == "RefT NullT"
+  "Class C" == "RefT (ClassT C)"
 
 end
diff -r 46db6fde4ee3 -r c7226e6f9625 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Mon Sep 25 12:04:10 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Mon Sep 25 12:08:49 2000 +0200
@@ -19,10 +19,10 @@
 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"
@@ -31,9 +31,9 @@
  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>
-	(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
-	(case sc of None => C = Object
+  (\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
+  (\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
+  (case sc of None => C = Object
          | Some D =>
              is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<preceq>C C \\<and>
              (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.