changeset 76217 | 8655344f1cf6 |
parent 76216 | 9fc34f76b4e8 |
--- a/src/ZF/UNITY/AllocBase.thy Tue Sep 27 17:54:20 2022 +0100 +++ b/src/ZF/UNITY/AllocBase.thy Tue Sep 27 18:02:34 2022 +0100 @@ -268,7 +268,7 @@ lemma part_ord_Lt [simp]: "part_ord(nat, Lt)" -apply (unfold part_ord_def Lt_def irrefl_def trans_on_def) + unfolding part_ord_def Lt_def irrefl_def trans_on_def apply (auto intro: lt_trans) done