avoid unnamed infixes;
authorwenzelm
Wed Oct 03 19:49:33 2007 +0200 (2007-10-03)
changeset 24824b7866aea0815
parent 24823 bfb619994060
child 24825 c4f13ab78f9d
avoid unnamed infixes;
src/HOL/Induct/Com.thy
src/HOL/Induct/PropLog.thy
     1.1 --- a/src/HOL/Induct/Com.thy	Wed Oct 03 19:36:05 2007 +0200
     1.2 +++ b/src/HOL/Induct/Com.thy	Wed Oct 03 19:49:33 2007 +0200
     1.3 @@ -11,20 +11,18 @@
     1.4  theory Com imports Main begin
     1.5  
     1.6  typedecl loc
     1.7 -
     1.8  types  state = "loc => nat"
     1.9 -       n2n2n = "nat => nat => nat"
    1.10  
    1.11  datatype
    1.12    exp = N nat
    1.13        | X loc
    1.14 -      | Op n2n2n exp exp
    1.15 +      | Op "nat => nat => nat" exp exp
    1.16        | valOf com exp          ("VALOF _ RESULTIS _"  60)
    1.17  and
    1.18    com = SKIP
    1.19 -      | ":="  loc exp          (infixl  60)
    1.20 -      | Semi  com com          ("_;;_"  [60, 60] 60)
    1.21 -      | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
    1.22 +      | Assign loc exp         (infixl ":=" 60)
    1.23 +      | Semi com com           ("_;;_"  [60, 60] 60)
    1.24 +      | Cond exp com com       ("IF _ THEN _ ELSE _"  60)
    1.25        | While exp com          ("WHILE _ DO _"  60)
    1.26  
    1.27  
     2.1 --- a/src/HOL/Induct/PropLog.thy	Wed Oct 03 19:36:05 2007 +0200
     2.2 +++ b/src/HOL/Induct/PropLog.thy	Wed Oct 03 19:49:33 2007 +0200
     2.3 @@ -21,8 +21,10 @@
     2.4  
     2.5  subsection {* The datatype of propositions *}
     2.6  
     2.7 -datatype
     2.8 -    'a pl = false | var 'a ("#_" [1000]) | "->" "'a pl" "'a pl" (infixr 90)
     2.9 +datatype 'a pl =
    2.10 +  false |
    2.11 +  var 'a ("#_" [1000]) |
    2.12 +  imp "'a pl" "'a pl" (infixr "->" 90)
    2.13  
    2.14  subsection {* The proof system *}
    2.15