equal
deleted
inserted
replaced
921 "(| pset = P, order = induced P r|) \<in> CompleteLattice" |
921 "(| pset = P, order = induced P r|) \<in> CompleteLattice" |
922 apply (rule CompleteLatticeI_simp) |
922 apply (rule CompleteLatticeI_simp) |
923 apply (rule fixf_po, clarify) |
923 apply (rule fixf_po, clarify) |
924 apply (simp add: P_def A_def r_def) |
924 apply (simp add: P_def A_def r_def) |
925 apply (rule Tarski.tarski_full_lemma [OF Tarski.intro [OF _ Tarski_axioms.intro]]) |
925 apply (rule Tarski.tarski_full_lemma [OF Tarski.intro [OF _ Tarski_axioms.intro]]) |
926 proof - show "CLF cl f" by unfold_locales qed |
926 proof - show "CLF cl f" .. qed |
927 |
927 |
928 end |
928 end |