equal
deleted
inserted
replaced
901 subsection \<open>Specification package -- Hilbertized version\<close> |
901 subsection \<open>Specification package -- Hilbertized version\<close> |
902 |
902 |
903 lemma exE_some: "Ex P \<Longrightarrow> c \<equiv> Eps P \<Longrightarrow> P c" |
903 lemma exE_some: "Ex P \<Longrightarrow> c \<equiv> Eps P \<Longrightarrow> P c" |
904 by (simp only: someI_ex) |
904 by (simp only: someI_ex) |
905 |
905 |
906 ML_file "Tools/choice_specification.ML" |
906 ML_file \<open>Tools/choice_specification.ML\<close> |
907 |
907 |
908 subsection \<open>Complete Distributive Lattices -- Properties depending on Hilbert Choice\<close> |
908 subsection \<open>Complete Distributive Lattices -- Properties depending on Hilbert Choice\<close> |
909 |
909 |
910 context complete_distrib_lattice |
910 context complete_distrib_lattice |
911 begin |
911 begin |