src/HOL/Bali/Term.thy
changeset 32960 69916a850301
parent 27226 5a3e5e46d977
child 35067 af4c18c30593
--- a/src/HOL/Bali/Term.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Bali/Term.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -67,8 +67,8 @@
         | Ret         --{* return from method *}
 
 datatype xcpt        --{* exception *}
-	= Loc loc    --{* location of allocated execption object *}
-	| Std xname  --{* intermediate standard exception, see Eval.thy *}
+        = Loc loc    --{* location of allocated execption object *}
+        | Std xname  --{* intermediate standard exception, see Eval.thy *}
 
 datatype error
        =  AccessViolation  --{* Access to a member that isn't permitted *}
@@ -92,12 +92,12 @@
  "locals" <= (type) "(lname, val) table"
 
 datatype inv_mode                  --{* invocation mode for method calls *}
-	= Static                   --{* static *}
-	| SuperM                   --{* super  *}
-	| IntVir                   --{* interface or virtual *}
+        = Static                   --{* static *}
+        | SuperM                   --{* super  *}
+        | IntVir                   --{* interface or virtual *}
 
 record  sig =              --{* signature of a method, cf. 8.4.2  *}
-	  name ::"mname"   --{* acutally belongs to Decl.thy *}
+          name ::"mname"   --{* acutally belongs to Decl.thy *}
           parTs::"ty list"        
 
 translations
@@ -142,7 +142,7 @@
 *}
 
 datatype var
-	= LVar lname --{* local variable (incl. parameters) *}
+        = LVar lname --{* local variable (incl. parameters) *}
         | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
                      --{* class field *}
                      --{* @{term "{accC,statDeclC,stat}e..fn"}   *}
@@ -153,7 +153,7 @@
                      --{* @{text stat}: static or instance field?*}
                      --{* @{text e}: reference to object*}
                      --{* @{text fn}: field name*}
-	| AVar expr expr ("_.[_]"[90,10   ]90)
+        | AVar expr expr ("_.[_]"[90,10   ]90)
                      --{* array component *}
                      --{* @{term "e1.[e2]"}: e1 array reference; e2 index *}
         | InsInitV stmt var 
@@ -161,21 +161,21 @@
                      --{* of var (technical term for smallstep semantics.)*}
 
 and expr
-	= NewC qtname         --{* class instance creation *}
-	| NewA ty expr ("New _[_]"[99,10   ]85) 
+        = NewC qtname         --{* class instance creation *}
+        | NewA ty expr ("New _[_]"[99,10   ]85) 
                               --{* array creation *} 
-	| Cast ty expr        --{* type cast  *}
-	| Inst expr ref_ty ("_ InstOf _"[85,99] 85)   
+        | Cast ty expr        --{* type cast  *}
+        | Inst expr ref_ty ("_ InstOf _"[85,99] 85)   
                               --{* instanceof *}     
-	| Lit  val              --{* literal value, references not allowed *}
+        | Lit  val              --{* literal value, references not allowed *}
         | UnOp unop expr        --{* unary operation *}
         | BinOp binop expr expr --{* binary operation *}
         
-	| Super               --{* special Super keyword *}
-	| Acc  var            --{* variable access *}
-	| Ass  var expr       ("_:=_"   [90,85   ]85)
+        | Super               --{* special Super keyword *}
+        | Acc  var            --{* variable access *}
+        | Ass  var expr       ("_:=_"   [90,85   ]85)
                               --{* variable assign *} 
-	| Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *}  
+        | Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *}  
         | Call qtname ref_ty inv_mode expr mname "(ty list)" "(expr list)"  
             ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) 
                     --{* method call *} 
@@ -198,25 +198,25 @@
         | Callee locals expr  --{* save callers locals in callee-Frame *}
                               --{* (technical term for smallstep semantics) *}
 and  stmt
-	= Skip                  --{* empty      statement *}
-	| Expr  expr            --{* expression statement *}
+        = Skip                  --{* empty      statement *}
+        | Expr  expr            --{* expression statement *}
         | Lab   jump stmt       ("_\<bullet> _" [      99,66]66)
                                 --{* labeled statement; handles break *}
-	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
-	| If'   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
-	| Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
+        | Comp  stmt stmt       ("_;; _"                  [      66,65]65)
+        | If'   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
+        | Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
         | Jmp jump              --{* break, continue, return *}
-	| Throw expr
+        | Throw expr
         | TryC  stmt qtname vname stmt ("Try _ Catch'(_ _') _"  [79,99,80,79]70)
              --{* @{term "Try c1 Catch(C vn) c2"} *} 
              --{* @{text c1}: block were exception may be thrown *}
              --{* @{text C}:  execption class to catch *}
              --{* @{text vn}: local name for exception used in @{text c2}*}
              --{* @{text c2}: block to execute when exception is cateched*}
-	| Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
+        | Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
         | FinA abopt stmt       --{* Save abruption of first statement *} 
                                 --{* technical term  for smallstep sem.) *}
-	| Init  qtname          --{* class initialization *}
+        | Init  qtname          --{* class initialization *}
 
 
 text {*