src/HOL/IMP/Transition.thy
changeset 12546 0c90e581379f
parent 12434 ff2efde4574d
child 12566 fe20540bcf93
     1.1 --- a/src/HOL/IMP/Transition.thy	Tue Dec 18 21:28:01 2001 +0100
     1.2 +++ b/src/HOL/IMP/Transition.thy	Wed Dec 19 00:26:04 2001 +0100
     1.3 @@ -28,12 +28,12 @@
     1.4    @{text option} part in configurations:
     1.5  *}
     1.6  syntax
     1.7 -  "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
     1.8 -  "@angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
     1.9 +  "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
    1.10 +  "_angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
    1.11  
    1.12  syntax (xsymbols)
    1.13 -  "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
    1.14 -  "@angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
    1.15 +  "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
    1.16 +  "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
    1.17  
    1.18  translations
    1.19    "\<langle>c,s\<rangle>" == "(Some c, s)"
    1.20 @@ -44,19 +44,19 @@
    1.21    iteration.
    1.22  *}
    1.23  syntax
    1.24 -  "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.25 +  "_evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.26      ("_ -1-> _" [60,60] 60)
    1.27 -  "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    1.28 +  "_evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    1.29      ("_ -_-> _" [60,60,60] 60)
    1.30 -  "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.31 +  "_evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.32      ("_ -*-> _" [60,60] 60)
    1.33  
    1.34  syntax (xsymbols)
    1.35 -  "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.36 +  "_evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.37      ("_ \<longrightarrow>\<^sub>1 _" [60,60] 61)
    1.38 -  "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    1.39 +  "_evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    1.40      ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60)
    1.41 -  "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.42 +  "_evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.43      ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [60,60] 60)
    1.44  
    1.45  translations