equal
deleted
inserted
replaced
1000 apply (drule lt_asym, auto) |
1000 apply (drule lt_asym, auto) |
1001 done |
1001 done |
1002 |
1002 |
1003 lemma tot_ord_Lt: "tot_ord(nat,Lt)" |
1003 lemma tot_ord_Lt: "tot_ord(nat,Lt)" |
1004 by (simp add: tot_ord_def linear_Lt part_ord_Lt) |
1004 by (simp add: tot_ord_def linear_Lt part_ord_Lt) |
|
1005 |
|
1006 lemma well_ord_Lt: "well_ord(nat,Lt)" |
|
1007 by (simp add: well_ord_def wf_Lt wf_imp_wf_on tot_ord_Lt) |
1005 |
1008 |
1006 |
1009 |
1007 |
1010 |
1008 ML {* |
1011 ML {* |
1009 val ordermap_def = thm "ordermap_def"; |
1012 val ordermap_def = thm "ordermap_def"; |
1115 val irrefl_Lt = thm "irrefl_Lt"; |
1118 val irrefl_Lt = thm "irrefl_Lt"; |
1116 val trans_Lt = thm "trans_Lt"; |
1119 val trans_Lt = thm "trans_Lt"; |
1117 val part_ord_Lt = thm "part_ord_Lt"; |
1120 val part_ord_Lt = thm "part_ord_Lt"; |
1118 val linear_Lt = thm "linear_Lt"; |
1121 val linear_Lt = thm "linear_Lt"; |
1119 val tot_ord_Lt = thm "tot_ord_Lt"; |
1122 val tot_ord_Lt = thm "tot_ord_Lt"; |
|
1123 val well_ord_Lt = thm "well_ord_Lt"; |
1120 *} |
1124 *} |
1121 |
1125 |
1122 end |
1126 end |