--- a/src/HOL/ex/rel.ML Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/ex/rel.ML Tue Jan 30 15:24:36 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/rel
+(* Title: HOL/ex/rel
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Domain, range of a relation or function -- NOT YET WORKING
@@ -11,9 +11,9 @@
val thy = extend_theory Univ.thy "Rel"
([], [], [], [],
[
- (["domain"], "('a * 'b)set => 'a set"),
- (["range2"], "('a * 'b)set => 'b set"),
- (["field"], "('a * 'a)set => 'a set")
+ (["domain"], "('a * 'b)set => 'a set"),
+ (["range2"], "('a * 'b)set => 'b set"),
+ (["field"], "('a * 'a)set => 'a set")
],
None)
[