src/HOL/IMP/Natural.thy
changeset 14565 c6dc17aab88a
parent 12546 0c90e581379f
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/IMP/Natural.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/IMP/Natural.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -17,6 +17,9 @@
     1.4  syntax (xsymbols)
     1.5    "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
     1.9 +
    1.10  text {*
    1.11    We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started 
    1.12    in state @{text s}, terminates in state @{text s'}}. Formally,