src/HOL/MicroJava/J/Type.thy
changeset 10069 c7226e6f9625
parent 10061 fe82134773dc
child 11026 a50365d21144
     1.1 --- a/src/HOL/MicroJava/J/Type.thy	Mon Sep 25 12:04:10 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Type.thy	Mon Sep 25 12:08:49 2000 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  arities cname, vnam, mname :: term
     1.6  
     1.7 -datatype vname		(* names for This pointer and local/field variables *)
     1.8 +datatype vname    (* names for This pointer and local/field variables *)
     1.9    = This
    1.10    | VName vnam
    1.11  
    1.12 @@ -23,8 +23,8 @@
    1.13    | Boolean
    1.14    | Integer
    1.15  
    1.16 -datatype ref_ty		(* reference type, cf. 4.3 *)
    1.17 -  = NullT		      (* null type, cf. 4.1 *)
    1.18 +datatype ref_ty   (* reference type, cf. 4.3 *)
    1.19 +  = NullT         (* null type, cf. 4.1 *)
    1.20    | ClassT cname  (* class type *)
    1.21  
    1.22  datatype ty       (* any type, cf. 4.1 *)
    1.23 @@ -33,10 +33,10 @@
    1.24  
    1.25  syntax
    1.26    NT    :: "          ty"
    1.27 -	Class	:: "cname  => ty"
    1.28 +  Class :: "cname  => ty"
    1.29  
    1.30  translations
    1.31 -	"NT"      == "RefT NullT"
    1.32 -	"Class C" == "RefT (ClassT C)"
    1.33 +  "NT"      == "RefT NullT"
    1.34 +  "Class C" == "RefT (ClassT C)"
    1.35  
    1.36  end