equal
deleted
inserted
replaced
482 by Auto_tac; |
482 by Auto_tac; |
483 by (resolve_tac [Follows_munion] 1); |
483 by (resolve_tac [Follows_munion] 1); |
484 by Auto_tac; |
484 by Auto_tac; |
485 qed "Follows_msetsum_UN"; |
485 qed "Follows_msetsum_UN"; |
486 |
486 |
487 Goalw [refl_def, Le_def] "refl(nat, Le)"; |
487 |
488 by Auto_tac; |
|
489 qed "refl_Le"; |
|
490 Addsimps [refl_Le]; |
|
491 |
|
492 Goalw [trans_on_def, Le_def] "trans[nat](Le)"; |
|
493 by Auto_tac; |
|
494 by (blast_tac (claset() addIs [le_trans]) 1); |
|
495 qed "trans_on_Le"; |
|
496 Addsimps [trans_on_Le]; |
|
497 |
|
498 Goalw [trans_def, Le_def] "trans(Le)"; |
|
499 by Auto_tac; |
|
500 by (blast_tac (claset() addIs [le_trans]) 1); |
|
501 qed "trans_Le"; |
|
502 Addsimps [trans_Le]; |
|
503 |
|
504 Goalw [antisym_def, Le_def] "antisym(Le)"; |
|
505 by Auto_tac; |
|
506 by (dtac le_imp_not_lt 1); |
|
507 by (auto_tac (claset(), simpset() addsimps [le_iff])); |
|
508 qed "antisym_Le"; |
|
509 Addsimps [antisym_Le]; |
|
510 |
|
511 Goalw [part_order_def] "part_order(nat, Le)"; |
|
512 by Auto_tac; |
|
513 qed "part_order_Le"; |
|
514 Addsimps [part_order_Le]; |
|