src/HOL/IMP/Com.thy
changeset 972 e61b058d58d2
parent 965 24eef3860714
child 977 5d57287e5e1e
     1.1 --- a/src/HOL/IMP/Com.thy	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/IMP/Com.thy	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -26,9 +26,9 @@
     1.4  
     1.5  (** Evaluation of arithmetic expressions **)
     1.6  consts  evala    :: "(aexp*state*nat)set"
     1.7 -       "@evala"  :: "[aexp,state,nat] => bool"	("<_,_>/ -a-> _"  [0,0,50] 50)
     1.8 +       "@evala"  :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _"  [0,0,50] 50)
     1.9  translations
    1.10 -    "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
    1.11 +    "<ae,sig> -a-> n" == "(ae,sig,n) : evala"
    1.12  inductive "evala"
    1.13    intrs 
    1.14      N   "<N(n),s> -a-> n"
    1.15 @@ -51,10 +51,10 @@
    1.16  
    1.17  (** Evaluation of boolean expressions **)
    1.18  consts evalb	:: "(bexp*state*bool)set"	
    1.19 -       "@evalb" :: "[bexp,state,bool] => bool"	("<_,_>/ -b-> _"  [0,0,50] 50)
    1.20 +       "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _"  [0,0,50] 50)
    1.21  
    1.22  translations
    1.23 -    "<be,sig> -b-> b" == "<be,sig,b> : evalb"
    1.24 +    "<be,sig> -b-> b" == "(be,sig,b) : evalb"
    1.25  
    1.26  inductive "evalb"
    1.27   intrs (*avoid clash with ML constructors true, false*)
    1.28 @@ -79,11 +79,11 @@
    1.29  
    1.30  (** Execution of commands **)
    1.31  consts  evalc    :: "(com*state*state)set"
    1.32 -        "@evalc" :: "[com,state,state] => bool"  ("<_,_>/ -c-> _" [0,0,50] 50)
    1.33 -	"assign" :: "[state,nat,loc] => state"   ("_[_'/_]"       [95,0,0] 95)
    1.34 +        "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50)
    1.35 +	"assign" :: "[state,nat,loc] => state"  ("_[_'/_]"       [95,0,0] 95)
    1.36  
    1.37  translations
    1.38 -       "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
    1.39 +       "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
    1.40  
    1.41  rules 
    1.42  	assign_def	"s[m/x] == (%y. if y=x then m else s y)"