--- a/src/HOLCF/Porder0.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Porder0.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/porder0.thy
+(* Title: HOLCF/porder0.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Definition of class porder (partial order)
@@ -20,24 +20,24 @@
arities void :: po
-consts "<<" :: "['a,'a::po] => bool" (infixl 55)
+consts "<<" :: "['a,'a::po] => bool" (infixl 55)
rules
(* class axioms: justification is theory Void *)
-refl_less "x << x"
- (* witness refl_less_void *)
+refl_less "x << x"
+ (* witness refl_less_void *)
-antisym_less "[|x<<y ; y<<x |] ==> x = y"
- (* witness antisym_less_void *)
+antisym_less "[|x<<y ; y<<x |] ==> x = y"
+ (* witness antisym_less_void *)
-trans_less "[|x<<y ; y<<z |] ==> x<<z"
- (* witness trans_less_void *)
+trans_less "[|x<<y ; y<<z |] ==> x<<z"
+ (* witness trans_less_void *)
(* instance of << for the prototype void *)
-inst_void_po "((op <<)::[void,void]=>bool) = less_void"
+inst_void_po "((op <<)::[void,void]=>bool) = less_void"
(* start 8bit 1 *)
(* end 8bit 1 *)