--- 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)
--- 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
--- 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'.