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.
comment;
authorwenzelm
Tue, 27 Oct 2009 15:02:31 +0100
changeset 33226 9a2911232c1b
parent 33225 0496565527bd
child 33227 83322d668601
child 33240 66eddea44a67
comment;
src/HOLCF/Tools/pcpodef.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Tools/pcpodef.ML	Tue Oct 27 13:34:37 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Tue Oct 27 15:02:31 2009 +0100
@@ -90,6 +90,7 @@
 
     fun make_cpo admissible (type_def, below_def, set_def) theory =
       let
+        (* FIXME fold_rule might fold user input inintentionally *)
         val admissible' = fold_rule (the_list set_def) admissible;
         val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
         val theory' = theory
@@ -112,6 +113,7 @@
 
     fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
       let
+        (* FIXME fold_rule might fold user input inintentionally *)
         val UU_mem' = fold_rule (the_list set_def) UU_mem;
         val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
         val theory' = theory
isabelle