1.1 --- a/src/HOL/IMPP/Com.thy	Wed Jun 25 21:25:51 2008 +0200
     1.2 +++ b/src/HOL/IMPP/Com.thy	Wed Jun 25 22:01:34 2008 +0200
     1.3 @@ -15,8 +15,8 @@
     1.4  typedecl glb
     1.5  typedecl loc
     1.6  
     1.7 -consts
     1.8 -  Arg :: loc
     1.9 +axiomatization
    1.10 +  Arg :: loc and
    1.11    Res :: loc
    1.12  
    1.13  datatype vname  = Glb glb | Loc loc
    1.14 @@ -43,8 +43,9 @@
    1.15        | Call  vname pname aexp  ("_:=CALL _'(_')"       [65, 65,  0] 60)
    1.16  
    1.17  consts bodies :: "(pname  *  com) list"(* finitely many procedure definitions *)
    1.18 -       body   :: " pname ~=> com"
    1.19 -defs   body_def: "body == map_of bodies"
    1.20 +definition
    1.21 +  body :: " pname ~=> com" where
    1.22 +  "body = map_of bodies"
    1.23  
    1.24  
    1.25  (* Well-typedness: all procedures called must exist *)
    1.26 @@ -78,9 +79,9 @@
    1.27    "WT (c1;;c2)"  "WT (IF b THEN c1 ELSE c2)"  "WT (WHILE b DO c)"
    1.28    "WT (BODY P)"  "WT (X:=CALL P(a))"
    1.29  
    1.30 -constdefs
    1.31 -  WT_bodies :: bool
    1.32 -  "WT_bodies == !(pn,b):set bodies. WT b"
    1.33 +definition
    1.34 +  WT_bodies :: bool where
    1.35 +  "WT_bodies = (!(pn,b):set bodies. WT b)"
    1.36  
    1.37  
    1.38  ML {* val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl] *}