Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
switch to transparent ascription, to avoid warning messages
authorhuffman
Sun, 19 Dec 2010 18:15:21 -0800
changeset 41296 6aaf80ea9715
parent 41295 5b5388d4ccc9
child 41297 01b2de947cff
switch to transparent ascription, to avoid warning messages
src/HOL/HOLCF/Tools/Domain/domain.ML file | annotate | diff | comparison | revisions
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML file | annotate | diff | comparison | revisions
src/HOL/HOLCF/Tools/Domain/domain_induction.ML file | annotate | diff | comparison | revisions
src/HOL/HOLCF/Tools/cont_proc.ML file | annotate | diff | comparison | revisions
src/HOL/HOLCF/Tools/cpodef.ML file | annotate | diff | comparison | revisions
src/HOL/HOLCF/Tools/domaindef.ML file | annotate | diff | comparison | revisions
src/HOL/HOLCF/Tools/fixrec.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -28,7 +28,7 @@
       -> theory -> theory
 end
 
-structure Domain :> DOMAIN =
+structure Domain : DOMAIN =
 struct
 
 open HOLCF_Library
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -34,7 +34,7 @@
 end
 
 
-structure Domain_Constructors :> DOMAIN_CONSTRUCTORS =
+structure Domain_Constructors : DOMAIN_CONSTRUCTORS =
 struct
 
 open HOLCF_Library
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -17,7 +17,7 @@
   val trace_domain: bool Unsynchronized.ref
 end
 
-structure Domain_Induction :> DOMAIN_INDUCTION =
+structure Domain_Induction : DOMAIN_INDUCTION =
 struct
 
 val quiet_mode = Unsynchronized.ref false
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -12,7 +12,7 @@
   val setup: theory -> theory
 end
 
-structure ContProc :> CONT_PROC =
+structure ContProc : CONT_PROC =
 struct
 
 (** theory context references **)
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -38,7 +38,7 @@
     * (binding * binding) option -> theory -> Proof.state
 end
 
-structure Cpodef :> CPODEF =
+structure Cpodef : CPODEF =
 struct
 
 (** type definitions **)
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -25,7 +25,7 @@
     * (binding * binding) option -> theory -> theory
 end
 
-structure Domaindef :> DOMAINDEF =
+structure Domaindef : DOMAINDEF =
 struct
 
 open HOLCF_Library
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -15,7 +15,7 @@
   val setup: theory -> theory
 end
 
-structure Fixrec :> FIXREC =
+structure Fixrec : FIXREC =
 struct
 
 open HOLCF_Library
isabelle