--- a/src/HOL/Bali/Example.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Bali/Example.thy Sat Oct 17 14:43:18 2009 +0200
@@ -170,11 +170,11 @@
Ext_foo :: mdecl
"Ext_foo \<equiv> (foo_sig,
\<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
- mbody=\<lparr>lcls=[]
+ mbody=\<lparr>lcls=[]
,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee :=
- Lit (Intg 1)) ;;
+ Lit (Intg 1)) ;;
Return (Lit Null)\<rparr>
- \<rparr>)"
+ \<rparr>)"
constdefs
@@ -184,7 +184,7 @@
BaseCl :: "class"
"BaseCl \<equiv> \<lparr>access=Public,
cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
- (vee, \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)],
+ (vee, \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)],
methods=[Base_foo],
init=Expr(arr_viewed_from Base Base
:=New (PrimT Boolean)[Lit (Intg 2)]),