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/Sprod.ML
changeset 15576 efb95d0d01f7
child 16059 dab0d004732f 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Sprod.ML	Fri Mar 04 23:12:36 2005 +0100
@@ -0,0 +1,101 @@
+
+(* legacy ML bindings *)
+
+val Ispair_def = thm "Ispair_def";
+val Isfst_def = thm "Isfst_def";
+val Issnd_def = thm "Issnd_def";
+val SprodI = thm "SprodI";
+val inj_on_Abs_Sprod = thm "inj_on_Abs_Sprod";
+val strict_Spair_Rep = thm "strict_Spair_Rep";
+val defined_Spair_Rep_rev = thm "defined_Spair_Rep_rev";
+val inject_Spair_Rep = thm "inject_Spair_Rep";
+val inject_Ispair = thm "inject_Ispair";
+val strict_Ispair = thm "strict_Ispair";
+val strict_Ispair1 = thm "strict_Ispair1";
+val strict_Ispair2 = thm "strict_Ispair2";
+val strict_Ispair_rev = thm "strict_Ispair_rev";
+val defined_Ispair_rev = thm "defined_Ispair_rev";
+val defined_Ispair = thm "defined_Ispair";
+val Exh_Sprod = thm "Exh_Sprod";
+val IsprodE = thm "IsprodE";
+val strict_Isfst = thm "strict_Isfst";
+val strict_Isfst1 = thm "strict_Isfst1";
+val strict_Isfst2 = thm "strict_Isfst2";
+val strict_Issnd = thm "strict_Issnd";
+val strict_Issnd1 = thm "strict_Issnd1";
+val strict_Issnd2 = thm "strict_Issnd2";
+val Isfst = thm "Isfst";
+val Issnd = thm "Issnd";
+val Isfst2 = thm "Isfst2";
+val Issnd2 = thm "Issnd2";
+val Sprod0_ss = [strict_Isfst1, strict_Isfst2, strict_Issnd1, strict_Issnd2,
+                 Isfst2, Issnd2]
+val defined_IsfstIssnd = thm "defined_IsfstIssnd";
+val surjective_pairing_Sprod = thm "surjective_pairing_Sprod";
+val Sel_injective_Sprod = thm "Sel_injective_Sprod";
+val less_sprod_def = thm "less_sprod_def";
+val refl_less_sprod = thm "refl_less_sprod";
+val antisym_less_sprod = thm "antisym_less_sprod";
+val trans_less_sprod = thm "trans_less_sprod";
+val inst_sprod_po = thm "inst_sprod_po";
+val minimal_sprod = thm "minimal_sprod";
+val UU_sprod_def = thm "UU_sprod_def";
+val least_sprod = thm "least_sprod";
+val monofun_Ispair1 = thm "monofun_Ispair1";
+val monofun_Ispair2 = thm "monofun_Ispair2";
+val monofun_Ispair = thm "monofun_Ispair";
+val monofun_Isfst = thm "monofun_Isfst";
+val monofun_Issnd = thm "monofun_Issnd";
+val lub_sprod = thm "lub_sprod";
+val thelub_sprod = thm "thelub_sprod";
+val cpo_sprod = thm "cpo_sprod";
+val spair_def = thm "spair_def";
+val sfst_def = thm "sfst_def";
+val ssnd_def = thm "ssnd_def";
+val ssplit_def = thm "ssplit_def";
+val inst_sprod_pcpo = thm "inst_sprod_pcpo";
+val sprod3_lemma1 = thm "sprod3_lemma1";
+val sprod3_lemma2 = thm "sprod3_lemma2";
+val sprod3_lemma3 = thm "sprod3_lemma3";
+val contlub_Ispair1 = thm "contlub_Ispair1";
+val sprod3_lemma4 = thm "sprod3_lemma4";
+val sprod3_lemma5 = thm "sprod3_lemma5";
+val sprod3_lemma6 = thm "sprod3_lemma6";
+val contlub_Ispair2 = thm "contlub_Ispair2";
+val cont_Ispair1 = thm "cont_Ispair1";
+val cont_Ispair2 = thm "cont_Ispair2";
+val contlub_Isfst = thm "contlub_Isfst";
+val contlub_Issnd = thm "contlub_Issnd";
+val cont_Isfst = thm "cont_Isfst";
+val cont_Issnd = thm "cont_Issnd";
+val spair_eq = thm "spair_eq";
+val beta_cfun_sprod = thm "beta_cfun_sprod";
+val inject_spair = thm "inject_spair";
+val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2";
+val strict_spair = thm "strict_spair";
+val strict_spair1 = thm "strict_spair1";
+val strict_spair2 = thm "strict_spair2";
+val strict_spair_rev = thm "strict_spair_rev";
+val defined_spair_rev = thm "defined_spair_rev";
+val defined_spair = thm "defined_spair";
+val Exh_Sprod2 = thm "Exh_Sprod2";
+val sprodE = thm "sprodE";
+val strict_sfst = thm "strict_sfst";
+val strict_sfst1 = thm "strict_sfst1";
+val strict_sfst2 = thm "strict_sfst2";
+val strict_ssnd = thm "strict_ssnd";
+val strict_ssnd1 = thm "strict_ssnd1";
+val strict_ssnd2 = thm "strict_ssnd2";
+val sfst2 = thm "sfst2";
+val ssnd2 = thm "ssnd2";
+val defined_sfstssnd = thm "defined_sfstssnd";
+val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
+val lub_sprod2 = thm "lub_sprod2";
+val thelub_sprod2 = thm "thelub_sprod2";
+val ssplit1 = thm "ssplit1";
+val ssplit2 = thm "ssplit2";
+val ssplit3 = thm "ssplit3";
+val Sprod_rews = [strict_sfst1, strict_sfst2,
+                strict_ssnd1, strict_ssnd2, sfst2, ssnd2, defined_spair,
+                ssplit1, ssplit2]
+
isabelle