src/ZF/IMP/Com.thy
changeset 1534 e8de1db81559
parent 1478 2b8c2a7547ab
child 1741 8b3de497b49d
     1.1 --- a/src/ZF/IMP/Com.thy	Mon Mar 04 17:24:51 1996 +0100
     1.2 +++ b/src/ZF/IMP/Com.thy	Tue Mar 05 10:54:55 1996 +0100
     1.3 @@ -17,8 +17,8 @@
     1.4  datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
     1.5    "aexp" = N ("n: nat")
     1.6           | X ("x: loc")
     1.7 -         | Op1 ("f: nat -> nat", "a : aexp")
     1.8 -         | Op2 ("f: (nat*nat) -> nat", "a0 : aexp", "a1 : aexp")
     1.9 +         | Op1 ("f : nat -> nat", "a : aexp")
    1.10 +         | Op2 ("f : (nat*nat) -> nat", "a0 : aexp", "a1 : aexp")
    1.11  
    1.12  
    1.13  (** Evaluation of arithmetic expressions **)
    1.14 @@ -29,7 +29,7 @@
    1.15  inductive
    1.16    domains "evala" <= "aexp * (loc -> nat) * nat"
    1.17    intrs 
    1.18 -    N   "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
    1.19 +    N   "[| n:nat;  sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
    1.20      X   "[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
    1.21      Op1 "[| <e,sigma> -a-> n;  f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
    1.22      Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] 
    1.23 @@ -44,7 +44,7 @@
    1.24  datatype <= "univ(aexp Un ((nat*nat)->bool) )"
    1.25    "bexp" = true
    1.26           | false
    1.27 -         | ROp  ("f: (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
    1.28 +         | ROp  ("f : (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
    1.29           | noti ("b : bexp")
    1.30           | andi ("b0 : bexp", "b1 : bexp")      (infixl 60)
    1.31           | ori  ("b0 : bexp", "b1 : bexp")      (infixl 60)