src/ZF/ex/Comb.thy

-(*  Title: 	ZF/ex/Comb.thy
+(*  Title:      ZF/ex/Comb.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson
+    Author:     Lawrence C Paulson
     Copyright   1994  University of Cambridge
 
 Combinatory Logic example: the Church-Rosser Theorem
 Curiously, combinators do not include free variables.
 

 (** Inductive definition of contractions, -1->
              and (multi-step) reductions, --->
 **)
 consts
   contract  :: i
-  "-1->"    :: [i,i] => o    			(infixl 50)
-  "--->"    :: [i,i] => o    			(infixl 50)
+  "-1->"    :: [i,i] => o                       (infixl 50)
+  "--->"    :: [i,i] => o                       (infixl 50)
 
 translations
   "p -1-> q" == "<p,q> : contract"
   "p ---> q" == "<p,q> : contract^*"
 

 (** Inductive definition of parallel contractions, =1=>
              and (multi-step) parallel reductions, ===>
 **)
 consts
   parcontract :: i
-  "=1=>"    :: [i,i] => o    			(infixl 50)
-  "===>"    :: [i,i] => o    			(infixl 50)
+  "=1=>"    :: [i,i] => o                       (infixl 50)
+  "===>"    :: [i,i] => o                       (infixl 50)
 
 translations
   "p =1=> q" == "<p,q> : parcontract"
   "p ===> q" == "<p,q> : parcontract^+"