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/Ssum.ML
changeset 15576 efb95d0d01f7
child 15607 30576c645e91 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Ssum.ML	Fri Mar 04 23:12:36 2005 +0100
@@ -0,0 +1,112 @@
+
+(* legacy ML bindings *)
+
+val Isinl_def = thm "Isinl_def";
+val Isinr_def = thm "Isinr_def";
+val Iwhen_def = thm "Iwhen_def";
+val SsumIl = thm "SsumIl";
+val SsumIr = thm "SsumIr";
+val inj_on_Abs_Ssum = thm "inj_on_Abs_Ssum";
+val strict_SinlSinr_Rep = thm "strict_SinlSinr_Rep";
+val strict_IsinlIsinr = thm "strict_IsinlIsinr";
+val noteq_SinlSinr_Rep = thm "noteq_SinlSinr_Rep";
+val noteq_IsinlIsinr = thm "noteq_IsinlIsinr";
+val inject_Sinl_Rep1 = thm "inject_Sinl_Rep1";
+val inject_Sinr_Rep1 = thm "inject_Sinr_Rep1";
+val inject_Sinl_Rep2 = thm "inject_Sinl_Rep2";
+val inject_Sinr_Rep2 = thm "inject_Sinr_Rep2";
+val inject_Sinl_Rep = thm "inject_Sinl_Rep";
+val inject_Sinr_Rep = thm "inject_Sinr_Rep";
+val inject_Isinl = thm "inject_Isinl";
+val inject_Isinr = thm "inject_Isinr";
+val inject_Isinl_rev = thm "inject_Isinl_rev";
+val inject_Isinr_rev = thm "inject_Isinr_rev";
+val Exh_Ssum = thm "Exh_Ssum";
+val IssumE = thm "IssumE";
+val IssumE2 = thm "IssumE2";
+val Iwhen1 = thm "Iwhen1";
+val Iwhen2 = thm "Iwhen2";
+val Iwhen3 = thm "Iwhen3";
+val less_ssum_def = thm "less_ssum_def";
+val less_ssum1a = thm "less_ssum1a";
+val less_ssum1b = thm "less_ssum1b";
+val less_ssum1c = thm "less_ssum1c";
+val less_ssum1d = thm "less_ssum1d";
+val less_ssum2a = thm "less_ssum2a";
+val less_ssum2b = thm "less_ssum2b";
+val less_ssum2c = thm "less_ssum2c";
+val less_ssum2d = thm "less_ssum2d";
+val refl_less_ssum = thm "refl_less_ssum";
+val antisym_less_ssum = thm "antisym_less_ssum";
+val trans_less_ssum = thm "trans_less_ssum";
+val inst_ssum_po = thm "inst_ssum_po";
+val less_ssum3a = thm "less_ssum3a";
+val less_ssum3b = thm "less_ssum3b";
+val less_ssum3c = thm "less_ssum3c";
+val less_ssum3d = thm "less_ssum3d";
+val minimal_ssum = thm "minimal_ssum";
+val UU_ssum_def = thm "UU_ssum_def";
+val least_ssum = thm "least_ssum";
+val monofun_Isinl = thm "monofun_Isinl";
+val monofun_Isinr = thm "monofun_Isinr";
+val monofun_Iwhen1 = thm "monofun_Iwhen1";
+val monofun_Iwhen2 = thm "monofun_Iwhen2";
+val monofun_Iwhen3 = thm "monofun_Iwhen3";
+val ssum_lemma1 = thm "ssum_lemma1";
+val ssum_lemma2 = thm "ssum_lemma2";
+val ssum_lemma3 = thm "ssum_lemma3";
+val ssum_lemma4 = thm "ssum_lemma4";
+val ssum_lemma5 = thm "ssum_lemma5";
+val ssum_lemma6 = thm "ssum_lemma6";
+val ssum_lemma7 = thm "ssum_lemma7";
+val ssum_lemma8 = thm "ssum_lemma8";
+val lub_ssum1a = thm "lub_ssum1a";
+val lub_ssum1b = thm "lub_ssum1b";
+val thelub_ssum1a = thm "thelub_ssum1a";
+val thelub_ssum1b = thm "thelub_ssum1b";
+val cpo_ssum = thm "cpo_ssum";
+val sinl_def = thm "sinl_def";
+val sinr_def = thm "sinr_def";
+val sscase_def = thm "sscase_def";
+val inst_ssum_pcpo = thm "inst_ssum_pcpo";
+val contlub_Isinl = thm "contlub_Isinl";
+val contlub_Isinr = thm "contlub_Isinr";
+val cont_Isinl = thm "cont_Isinl";
+val cont_Isinr = thm "cont_Isinr";
+val contlub_Iwhen1 = thm "contlub_Iwhen1";
+val contlub_Iwhen2 = thm "contlub_Iwhen2";
+val ssum_lemma9 = thm "ssum_lemma9";
+val ssum_lemma10 = thm "ssum_lemma10";
+val ssum_lemma11 = thm "ssum_lemma11";
+val ssum_lemma12 = thm "ssum_lemma12";
+val ssum_lemma13 = thm "ssum_lemma13";
+val contlub_Iwhen3 = thm "contlub_Iwhen3";
+val cont_Iwhen1 = thm "cont_Iwhen1";
+val cont_Iwhen2 = thm "cont_Iwhen2";
+val cont_Iwhen3 = thm "cont_Iwhen3";
+val strict_sinl = thm "strict_sinl";
+val strict_sinr = thm "strict_sinr";
+val noteq_sinlsinr = thm "noteq_sinlsinr";
+val inject_sinl = thm "inject_sinl";
+val inject_sinr = thm "inject_sinr";
+val defined_sinl = thm "defined_sinl";
+val defined_sinr = thm "defined_sinr";
+val Exh_Ssum1 = thm "Exh_Ssum1";
+val ssumE = thm "ssumE";
+val ssumE2 = thm "ssumE2";
+val sscase1 = thm "sscase1";
+val sscase2 = thm "sscase2";
+val sscase3 = thm "sscase3";
+val less_ssum4a = thm "less_ssum4a";
+val less_ssum4b = thm "less_ssum4b";
+val less_ssum4c = thm "less_ssum4c";
+val less_ssum4d = thm "less_ssum4d";
+val ssum_chainE = thm "ssum_chainE";
+val thelub_ssum2a = thm "thelub_ssum2a";
+val thelub_ssum2b = thm "thelub_ssum2b";
+val thelub_ssum2a_rev = thm "thelub_ssum2a_rev";
+val thelub_ssum2b_rev = thm "thelub_ssum2b_rev";
+val thelub_ssum3 = thm "thelub_ssum3";
+val sscase4 = thm "sscase4";
+val Ssum_rews = [strict_sinl, strict_sinr, defined_sinl, defined_sinr,
+                sscase1, sscase2, sscase3]
isabelle