src/HOL/HOL.thy
 changeset 31173 bbe9e29b9672 parent 31172 74d72ba262fb parent 31166 a90fe83f58ea child 31299 0c5baf034d0e
equal inserted replaced
31172:74d72ba262fb 31173:bbe9e29b9672
`  1048     "(P & ~P) = False"    "(~P & P) = False"`
`  1048     "(P & ~P) = False"    "(~P & P) = False"`
`  1049     "(P | True) = True"  "(True | P) = True"`
`  1049     "(P | True) = True"  "(True | P) = True"`
`  1050     "(P | False) = P"  "(False | P) = P"`
`  1050     "(P | False) = P"  "(False | P) = P"`
`  1051     "(P | P) = P"  "(P | (P | Q)) = (P | Q)" and`
`  1051     "(P | P) = P"  "(P | (P | Q)) = (P | Q)" and`
`  1052     "(ALL x. P) = P"  "(EX x. P) = P"  "EX x. x=t"  "EX x. t=x"`
`  1052     "(ALL x. P) = P"  "(EX x. P) = P"  "EX x. x=t"  "EX x. t=x"`
`  1053     -- {* needed for the one-point-rule quantifier simplification procs *}`
`  1053   and`
`  1054     -- {* essential for termination!! *} and`
`       `
`  1055     "!!P. (EX x. x=t & P(x)) = P(t)"`
`  1054     "!!P. (EX x. x=t & P(x)) = P(t)"`
`  1056     "!!P. (EX x. t=x & P(x)) = P(t)"`
`  1055     "!!P. (EX x. t=x & P(x)) = P(t)"`
`  1057     "!!P. (ALL x. x=t --> P(x)) = P(t)"`
`  1056     "!!P. (ALL x. x=t --> P(x)) = P(t)"`
`  1058     "!!P. (ALL x. t=x --> P(x)) = P(t)"`
`  1057     "!!P. (ALL x. t=x --> P(x)) = P(t)"`
`  1059   by (blast, blast, blast, blast, blast, iprover+)`
`  1058   by (blast, blast, blast, blast, blast, iprover+)`