src/HOL/IMP/Com.thy
changeset 27362 a6dc1769fdda
parent 16417 9bc16273c2d4
child 41589 bbd861837ebc
     1.1 --- a/src/HOL/IMP/Com.thy	Wed Jun 25 21:25:51 2008 +0200
     1.2 +++ b/src/HOL/IMP/Com.thy	Wed Jun 25 22:01:34 2008 +0200
     1.3 @@ -28,9 +28,9 @@
     1.4        | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
     1.5        | While  bexp com         ("WHILE _ DO _"  60)
     1.6  
     1.7 -syntax (latex)
     1.8 -  SKIP :: com   ("\<SKIP>")
     1.9 -  Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com"  ("\<IF> _ \<THEN> _ \<ELSE> _"  60)
    1.10 -  While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _"  60)
    1.11 +notation (latex)
    1.12 +  SKIP  ("\<SKIP>") and
    1.13 +  Cond  ("\<IF> _ \<THEN> _ \<ELSE> _"  60) and
    1.14 +  While  ("\<WHILE> _ \<DO> _"  60)
    1.15  
    1.16  end