src/HOL/HOL.thy
 changeset 58830 e05c620eceeb parent 58826 2ed2eaabe3df child 58839 ccda99401bc8
equal inserted replaced
58829:38340f6e971e 58830:e05c620eceeb
`  1690 text {*`
`  1690 text {*`
`  1691  The simplification procedure can be used to avoid simplification of terms of a certain form`
`  1691  The simplification procedure can be used to avoid simplification of terms of a certain form`
`  1692 *}`
`  1692 *}`
`  1693 `
`  1693 `
`  1694 definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"`
`  1694 definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"`
`       `
`  1695 `
`  1695 lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)`
`  1696 lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)`
`       `
`  1697 `
`       `
`  1698 declare [[coercion_args NO_MATCH - -]]`
`  1696 `
`  1699 `
`  1697 simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>`
`  1700 simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>`
`  1698   let`
`  1701   let`
`  1699     val thy = Proof_Context.theory_of ctxt`
`  1702     val thy = Proof_Context.theory_of ctxt`
`  1700     val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)`
`  1703     val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)`