equal
deleted
inserted
replaced
45 abbreviation. Lemma monotone_def is explicitly provided for backward |
45 abbreviation. Lemma monotone_def is explicitly provided for backward |
46 compatibility but its usage is discouraged. Minor INCOMPATIBILITY. |
46 compatibility but its usage is discouraged. Minor INCOMPATIBILITY. |
47 - Added lemmas. |
47 - Added lemmas. |
48 monotone_onD |
48 monotone_onD |
49 monotone_onI |
49 monotone_onI |
|
50 monotone_on_empty[simp] |
|
51 monotone_on_subset |
50 |
52 |
51 * Theory "HOL.Relation": |
53 * Theory "HOL.Relation": |
52 - Added predicate reflp_on and redefined reflp to be an abbreviation. |
54 - Added predicate reflp_on and redefined reflp to be an abbreviation. |
53 Lemma reflp_def is explicitly provided for backward compatibility |
55 Lemma reflp_def is explicitly provided for backward compatibility |
54 but its usage is discouraged. Minor INCOMPATIBILITY. |
56 but its usage is discouraged. Minor INCOMPATIBILITY. |