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/HOLCF/Fix.ML
changeset 18074 a92b7c5133de
parent 16922 2128ac2aa5db 
--- a/src/HOLCF/Fix.ML	Thu Nov 03 00:32:47 2005 +0100
+++ b/src/HOLCF/Fix.ML	Thu Nov 03 00:43:11 2005 +0100
@@ -6,11 +6,6 @@
 val admw_def = thm "admw_def";
 val chain_iterate2 = thm "chain_iterate2";
 val chain_iterate = thm "chain_iterate";
-val cont_Ifix = thm "cont_Ifix";
-val cont_iterate1 = thm "cont_iterate1";
-val cont_iterate2 = thm "cont_iterate2";
-val cont_iterate = thm "cont_iterate";
-val contlub_iterate2 = thm "contlub_iterate2";
 val def_fix_ind = thm "def_fix_ind";
 val def_wfix_ind = thm "def_wfix_ind";
 val fix_const = thm "fix_const";
@@ -28,19 +23,14 @@
 val fix_ind = thm "fix_ind";
 val fix_least = thm "fix_least";
 val fix_strict = thm "fix_strict";
-val Ifix_def = thm "Ifix_def";
-val Ifix_eq = thm "Ifix_eq";
-val Ifix_least = thm "Ifix_least";
 val iterate_0 = thm "iterate_0";
 val iterate_Suc2 = thm "iterate_Suc2";
 val iterate_Suc = thm "iterate_Suc";
-val monofun_iterate2 = thm "monofun_iterate2";
 val wfix_ind = thm "wfix_ind";
 
 structure Fix =
 struct
   val thy = the_context ();
-  val Ifix_def = Ifix_def;
   val fix_def = fix_def;
   val adm_def = adm_def;
   val admw_def = admw_def;
isabelle