src/HOL/simpdata.ML
 changeset 11162 9e2ec5f02217 parent 11034 568eb11f8d52 child 11200 f43fa07536c0
equal inserted replaced
11161:166f7d87b37f 11162:9e2ec5f02217
`   328   might cause exponential blow-up.  But imp_disjL has been in for a while`
`   328   might cause exponential blow-up.  But imp_disjL has been in for a while`
`   329   and cannot be removed without affecting existing proofs.  Moreover,`
`   329   and cannot be removed without affecting existing proofs.  Moreover,`
`   330   rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the`
`   330   rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the`
`   331   grounds that it allows simplification of R in the two cases.*)`
`   331   grounds that it allows simplification of R in the two cases.*)`
`   332 `
`   332 `
`   335 val mksimps_pairs =`
`   333 val mksimps_pairs =`
`   336   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),`
`   334   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),`
`   337    ("All", [spec]), ("True", []), ("False", []),`
`   335    ("All", [spec]), ("True", []), ("False", []),`
`   338    ("If", [if_bool_eq_conj RS iffD1])];`
`   336    ("If", [if_bool_eq_conj RS iffD1])];`
`   339 `
`   337 `
`   352                    | None => [th])`
`   350                    | None => [th])`
`   353               | _ => [th])`
`   351               | _ => [th])`
`   354          | _ => [th])`
`   352          | _ => [th])`
`   355   in atoms end;`
`   353   in atoms end;`
`   356 `
`   354 `
`   357 fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);`
`   355 fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe);`
`   358 `
`   356 `
`   359 fun unsafe_solver_tac prems =`
`   357 fun unsafe_solver_tac prems =`
`   360   FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];`
`   358   FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];`
`   361 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;`
`   359 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;`
`   362 `
`   360 `