src/HOL/Bali/Example.thy
changeset 32960 69916a850301
parent 32456 341c83339aeb
child 33965 f57c11db4ad4
     1.1 --- a/src/HOL/Bali/Example.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -170,11 +170,11 @@
     1.4    Ext_foo  :: mdecl
     1.5   "Ext_foo  \<equiv> (foo_sig, 
     1.6                \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
     1.7 -	       mbody=\<lparr>lcls=[]
     1.8 +               mbody=\<lparr>lcls=[]
     1.9                       ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
    1.10 -       	                                                     Lit (Intg 1)) ;;
    1.11 +                                                             Lit (Intg 1)) ;;
    1.12                                  Return (Lit Null)\<rparr>
    1.13 -	      \<rparr>)"
    1.14 +              \<rparr>)"
    1.15  
    1.16  constdefs
    1.17    
    1.18 @@ -184,7 +184,7 @@
    1.19  BaseCl :: "class"
    1.20  "BaseCl \<equiv> \<lparr>access=Public,
    1.21             cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
    1.22 -	            (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
    1.23 +                    (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
    1.24             methods=[Base_foo],
    1.25             init=Expr(arr_viewed_from Base Base 
    1.26                       :=New (PrimT Boolean)[Lit (Intg 2)]),