src/ZF/IMP/Com.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/IMP/Com.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/IMP/Com.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -11,8 +11,8 @@
     1.4  Com = Datatype +
     1.5  
     1.6  (** Arithmetic expressions **)
     1.7 -consts  loc  :: "i"
     1.8 -        aexp :: "i"
     1.9 +consts  loc  :: i
    1.10 +        aexp :: i
    1.11  
    1.12  datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
    1.13    "aexp" = N ("n: nat")
    1.14 @@ -22,8 +22,8 @@
    1.15  
    1.16  
    1.17  (** Evaluation of arithmetic expressions **)
    1.18 -consts  evala    :: "i"
    1.19 -       "@evala"  :: "[i,i,i] => o"		("<_,_>/ -a-> _"  [0,0,50] 50)
    1.20 +consts  evala    :: i
    1.21 +       "@evala"  :: [i,i,i] => o		("<_,_>/ -a-> _"  [0,0,50] 50)
    1.22  translations
    1.23      "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
    1.24  inductive
    1.25 @@ -39,7 +39,7 @@
    1.26  
    1.27  
    1.28  (** Boolean expressions **)
    1.29 -consts  bexp :: "i"
    1.30 +consts  bexp :: i
    1.31  
    1.32  datatype <= "univ(aexp Un ((nat*nat)->bool) )"
    1.33    "bexp" = true
    1.34 @@ -51,8 +51,8 @@
    1.35  
    1.36  
    1.37  (** Evaluation of boolean expressions **)
    1.38 -consts evalb	:: "i"	
    1.39 -       "@evalb" :: "[i,i,i] => o"		("<_,_>/ -b-> _" [0,0,50] 50)
    1.40 +consts evalb	:: i	
    1.41 +       "@evalb" :: [i,i,i] => o		("<_,_>/ -b-> _" [0,0,50] 50)
    1.42  
    1.43  translations
    1.44      "<be,sig> -b-> b" == "<be,sig,b> : evalb"
    1.45 @@ -76,7 +76,7 @@
    1.46  
    1.47  
    1.48  (** Commands **)
    1.49 -consts  com :: "i"
    1.50 +consts  com :: i
    1.51  
    1.52  datatype <= "univ(loc Un aexp Un bexp)"
    1.53    "com" = skip
    1.54 @@ -89,9 +89,9 @@
    1.55    with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)
    1.56  
    1.57  (** Execution of commands **)
    1.58 -consts  evalc    :: "i"
    1.59 -        "@evalc" :: "[i,i,i] => o"   		("<_,_>/ -c-> _" [0,0,50] 50)
    1.60 -	"assign" :: "[i,i,i] => i"   		("_[_'/_]"       [95,0,0] 95)
    1.61 +consts  evalc    :: i
    1.62 +        "@evalc" :: [i,i,i] => o   		("<_,_>/ -c-> _" [0,0,50] 50)
    1.63 +	"assign" :: [i,i,i] => i   		("_[_'/_]"       [95,0,0] 95)
    1.64  
    1.65  translations
    1.66         "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"