src/HOL/HOL.thy
 changeset 59864 c777743294e1 parent 59779 b6bda9140e39 child 59929 a090551e5ec8
equal inserted replaced
59863:30519ff3dffb 59864:c777743294e1
`  1262 next`
`  1262 next`
`  1263   assume "PROP P"`
`  1263   assume "PROP P"`
`  1264   then show "PROP P" .`
`  1264   then show "PROP P" .`
`  1265 qed`
`  1265 qed`
`  1266 `
`  1266 `
`       `
`  1267 lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"`
`       `
`  1268 by default (intro TrueI)`
`       `
`  1269 `
`       `
`  1270 lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"`
`       `
`  1271 by default simp_all`
`       `
`  1272 `
`  1267 lemma ex_simps:`
`  1273 lemma ex_simps:`
`  1268   "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"`
`  1274   "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"`
`  1269   "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"`
`  1275   "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"`
`  1270   "!!P Q. (EX x. P x | Q)   = ((EX x. P x) | Q)"`
`  1276   "!!P Q. (EX x. P x | Q)   = ((EX x. P x) | Q)"`
`  1271   "!!P Q. (EX x. P | Q x)   = (P | (EX x. Q x))"`
`  1277   "!!P Q. (EX x. P | Q x)   = (P | (EX x. Q x))"`