equal
deleted
inserted
replaced
920 val Ord_in_Ord' = thm "Ord_in_Ord'"; |
920 val Ord_in_Ord' = thm "Ord_in_Ord'"; |
921 val le_well_ord_Memrel = thm "le_well_ord_Memrel"; |
921 val le_well_ord_Memrel = thm "le_well_ord_Memrel"; |
922 val well_ord_Memrel = thm "well_ord_Memrel"; |
922 val well_ord_Memrel = thm "well_ord_Memrel"; |
923 val lt_pred_Memrel = thm "lt_pred_Memrel"; |
923 val lt_pred_Memrel = thm "lt_pred_Memrel"; |
924 val pred_Memrel = thm "pred_Memrel"; |
924 val pred_Memrel = thm "pred_Memrel"; |
925 val Ord_iso_implies_eq_lemma = thm "Ord_iso_implies_eq_lemma"; |
|
926 val Ord_iso_implies_eq = thm "Ord_iso_implies_eq"; |
925 val Ord_iso_implies_eq = thm "Ord_iso_implies_eq"; |
927 val ordermap_type = thm "ordermap_type"; |
926 val ordermap_type = thm "ordermap_type"; |
928 val ordermap_eq_image = thm "ordermap_eq_image"; |
927 val ordermap_eq_image = thm "ordermap_eq_image"; |
929 val ordermap_pred_unfold = thm "ordermap_pred_unfold"; |
928 val ordermap_pred_unfold = thm "ordermap_pred_unfold"; |
930 val ordermap_unfold = thm "ordermap_unfold"; |
929 val ordermap_unfold = thm "ordermap_unfold"; |
994 val odiff_oadd_inverse = thm "odiff_oadd_inverse"; |
993 val odiff_oadd_inverse = thm "odiff_oadd_inverse"; |
995 val odiff_lt_mono2 = thm "odiff_lt_mono2"; |
994 val odiff_lt_mono2 = thm "odiff_lt_mono2"; |
996 val Ord_omult = thm "Ord_omult"; |
995 val Ord_omult = thm "Ord_omult"; |
997 val pred_Pair_eq = thm "pred_Pair_eq"; |
996 val pred_Pair_eq = thm "pred_Pair_eq"; |
998 val ordertype_pred_Pair_eq = thm "ordertype_pred_Pair_eq"; |
997 val ordertype_pred_Pair_eq = thm "ordertype_pred_Pair_eq"; |
999 val ordertype_pred_Pair_lemma = thm "ordertype_pred_Pair_lemma"; |
|
1000 val lt_omult = thm "lt_omult"; |
998 val lt_omult = thm "lt_omult"; |
1001 val omult_oadd_lt = thm "omult_oadd_lt"; |
999 val omult_oadd_lt = thm "omult_oadd_lt"; |
1002 val omult_unfold = thm "omult_unfold"; |
1000 val omult_unfold = thm "omult_unfold"; |
1003 val omult_0 = thm "omult_0"; |
1001 val omult_0 = thm "omult_0"; |
1004 val omult_0_left = thm "omult_0_left"; |
1002 val omult_0_left = thm "omult_0_left"; |