src/HOL/HOL.thy
changeset 58830 e05c620eceeb
parent 58826 2ed2eaabe3df
child 58839 ccda99401bc8
equal deleted 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)