# HG changeset patch
# User paulson
# Date 826019695 -3600
# Node ID e8de1db81559cbb349cff8868756fd3791974d61
# Parent  771474fd33be039375210c809d0a6aa50eba38ed
A mere adjustment of spacing

diff -r 771474fd33be -r e8de1db81559 src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Mon Mar 04 17:24:51 1996 +0100
+++ b/src/ZF/IMP/Com.thy	Tue Mar 05 10:54:55 1996 +0100
@@ -17,8 +17,8 @@
 datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
   "aexp" = N ("n: nat")
          | X ("x: loc")
-         | Op1 ("f: nat -> nat", "a : aexp")
-         | Op2 ("f: (nat*nat) -> nat", "a0 : aexp", "a1 : aexp")
+         | Op1 ("f : nat -> nat", "a : aexp")
+         | Op2 ("f : (nat*nat) -> nat", "a0 : aexp", "a1 : aexp")
 
 
 (** Evaluation of arithmetic expressions **)
@@ -29,7 +29,7 @@
 inductive
   domains "evala" <= "aexp * (loc -> nat) * nat"
   intrs 
-    N   "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
+    N   "[| n:nat;  sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
     X   "[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
     Op1 "[| <e,sigma> -a-> n;  f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
     Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] 
@@ -44,7 +44,7 @@
 datatype <= "univ(aexp Un ((nat*nat)->bool) )"
   "bexp" = true
          | false
-         | ROp  ("f: (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
+         | ROp  ("f : (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
          | noti ("b : bexp")
          | andi ("b0 : bexp", "b1 : bexp")      (infixl 60)
          | ori  ("b0 : bexp", "b1 : bexp")      (infixl 60)