do translation: CONST;
authorwenzelm
Fri Apr 13 21:26:34 2007 +0200 (2007-04-13)
changeset 22664e965391e2864
parent 22663 73517244fc46
child 22665 cf152ff55d16
do translation: CONST;
src/HOL/Library/State_Monad.thy
     1.1 --- a/src/HOL/Library/State_Monad.thy	Fri Apr 13 20:23:18 2007 +0200
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Apr 13 21:26:34 2007 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4      ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
     1.5  
     1.6  translations
     1.7 -  "_do f" => "State_Monad.run f"
     1.8 +  "_do f" => "CONST run f"
     1.9    "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
    1.10    "_fcomp f g" => "f \<guillemotright> g"
    1.11    "_let x t f" => "Let t (\<lambda>x. f)"
    1.12 @@ -307,4 +307,4 @@
    1.13    For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
    1.14  *}
    1.15  
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end