Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/FOL/simpdata.ML
changeset 36599 ca42a56e3b14
parent 36546 a9873318fe30
child 38500 d5477ee35820 
--- a/src/FOL/simpdata.ML	Fri Apr 30 09:54:04 2010 -0700
+++ b/src/FOL/simpdata.ML	Fri Apr 30 21:10:57 2010 +0200
@@ -35,10 +35,6 @@
   [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
    ("All", [@{thm spec}]), ("True", []), ("False", [])];
 
-(* ###FIXME: move to simplifier.ML
-val mk_atomize:      (string * thm list) list -> thm -> thm list
-*)
-(* ###FIXME: move to simplifier.ML *)
 fun mk_atomize pairs =
   let fun atoms th =
         (case concl_of th of
isabelle