--- 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*)
--- 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*)
--- 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
--- 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
-
--- 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
-