1.1 --- a/src/HOL/Bali/Example.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Bali/Example.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -87,31 +87,39 @@
     1.4    surj_label_:" \<exists>m. n = label_ m"
     1.5  
     1.6  abbreviation
     1.7 -  HasFoo :: qtname
     1.8 +  HasFoo :: qtname where
     1.9    "HasFoo == \<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
    1.10  
    1.11 -  Base :: qtname
    1.12 +abbreviation
    1.13 +  Base :: qtname where
    1.14    "Base == \<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
    1.15  
    1.16 -  Ext :: qtname
    1.17 +abbreviation
    1.18 +  Ext :: qtname where
    1.19    "Ext == \<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
    1.20  
    1.21 -  Main :: qtname
    1.22 +abbreviation
    1.23 +  Main :: qtname where
    1.24    "Main == \<lparr>pid=java_lang,tid=TName (tnam_ Main_)\<rparr>"
    1.25  
    1.26 -  arr :: vname
    1.27 +abbreviation
    1.28 +  arr :: vname where
    1.29    "arr == (vnam_ arr_)"
    1.30  
    1.31 -  vee :: vname
    1.32 +abbreviation
    1.33 +  vee :: vname where
    1.34    "vee == (vnam_ vee_)"
    1.35  
    1.36 -  z :: vname
    1.37 +abbreviation
    1.38 +  z :: vname where
    1.39    "z == (vnam_ z_)"
    1.40  
    1.41 -  e :: vname
    1.42 +abbreviation
    1.43 +  e :: vname where
    1.44    "e == (vnam_ e_)"
    1.45  
    1.46 -  lab1:: label
    1.47 +abbreviation
    1.48 +  lab1:: label where
    1.49    "lab1 == label_ lab1_"
    1.50  
    1.51  
    1.52 @@ -261,7 +269,7 @@
    1.53  section "program"
    1.54  
    1.55  abbreviation
    1.56 -  tprg :: prog
    1.57 +  tprg :: prog where
    1.58    "tprg == \<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
    1.59  
    1.60  constdefs
    1.61 @@ -1195,11 +1203,10 @@
    1.62    b :: loc
    1.63    c :: loc
    1.64  
    1.65 -abbreviation
    1.66 -  "one == Suc 0"
    1.67 -  "two == Suc one"
    1.68 -  "tree == Suc two"
    1.69 -  "four == Suc tree"
    1.70 +abbreviation "one == Suc 0"
    1.71 +abbreviation "two == Suc one"
    1.72 +abbreviation "tree == Suc two"
    1.73 +abbreviation "four == Suc tree"
    1.74  
    1.75  syntax
    1.76    obj_a :: obj