# HG changeset patch
# User wenzelm
# Date 921674854 -3600
# Node ID 8b0c9205da75870489c4412f4f06c7de6a197509
# Parent  ed0c7b4a325def33ce251af78b885449f943aa0c
fixed typedef representing set;

diff -r ed0c7b4a325d -r 8b0c9205da75 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Wed Mar 17 13:47:04 1999 +0100
+++ b/src/HOL/Induct/LList.thy	Wed Mar 17 13:47:34 1999 +0100
@@ -44,7 +44,7 @@
 
 
 typedef (LList)
-  'a llist = "llist(range Leaf)" (llist.NIL_I)
+  'a llist = "llist(range Leaf) :: 'a item set" (llist.NIL_I)
 
 constdefs
   (*Now used exclusively for abbreviating the coinduction rule*)
diff -r ed0c7b4a325d -r 8b0c9205da75 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Wed Mar 17 13:47:04 1999 +0100
+++ b/src/HOL/Induct/SList.thy	Wed Mar 17 13:47:34 1999 +0100
@@ -33,7 +33,7 @@
 
 
 typedef (List)
-  'a list = "list(range Leaf)" (list.NIL_I)
+  'a list = "list(range Leaf) :: 'a item set" (list.NIL_I)
 
   
 (*Declaring the abstract list constructors*)
diff -r ed0c7b4a325d -r 8b0c9205da75 src/HOLCF/Cfun1.thy
--- a/src/HOLCF/Cfun1.thy	Wed Mar 17 13:47:04 1999 +0100
+++ b/src/HOLCF/Cfun1.thy	Wed Mar 17 13:47:34 1999 +0100
@@ -1,9 +1,9 @@
-(*  Title:      HOLCF/cfun1.thy
+(*  Title:      HOLCF/Cfun1.thy
     ID:         $Id$
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Definition of the type ->  of continuous functions
+Definition of the type ->  of continuous functions.
 
 *)
 
@@ -11,7 +11,7 @@
 
 default cpo
 
-typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f. cont f}" (CfunI)
+typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}" (CfunI)
 
 (* to make << defineable *)
 instance "->"  :: (cpo,cpo)sq_ord
diff -r ed0c7b4a325d -r 8b0c9205da75 src/HOLCF/Sprod0.thy
--- a/src/HOLCF/Sprod0.thy	Wed Mar 17 13:47:04 1999 +0100
+++ b/src/HOLCF/Sprod0.thy	Wed Mar 17 13:47:34 1999 +0100
@@ -3,7 +3,7 @@
     Author:     Franz Regensburger
     Copyright   1993  Technische Universitaet Muenchen
 
-Strict product with typedef
+Strict product with typedef.
 *)
 
 Sprod0 = Cfun3 +
@@ -12,7 +12,7 @@
   Spair_Rep     :: ['a,'b] => ['a,'b] => bool
  "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
 
-typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep a b}"
+typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
 
 syntax (symbols)
   "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
@@ -35,4 +35,3 @@
 
 
 end
-
diff -r ed0c7b4a325d -r 8b0c9205da75 src/HOLCF/Ssum0.thy
--- a/src/HOLCF/Ssum0.thy	Wed Mar 17 13:47:04 1999 +0100
+++ b/src/HOLCF/Ssum0.thy	Wed Mar 17 13:47:34 1999 +0100
@@ -15,7 +15,7 @@
  "Sinr_Rep == (%b.%x y p.(b~=UU --> y=b & ~p))"
 
 typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
-	"{f.(? a. f=Sinl_Rep(a))|(? b. f=Sinr_Rep(b))}"
+	"{f.(? a. f=Sinl_Rep(a::'a))|(? b. f=Sinr_Rep(b::'b))}"
 
 syntax (symbols)
   "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
@@ -35,4 +35,3 @@
                         &(!b. b~=UU & s=Isinr(b) --> z=g`b)"  
 
 end
-