author | hoelzl |
Thu, 30 Oct 2014 09:15:54 +0100 | |
changeset 58830 | e05c620eceeb |
parent 58829 | 38340f6e971e |
child 58831 | aa8cf5eed06e |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/HOL.thy Wed Oct 29 19:26:05 2014 +0100 +++ b/src/HOL/HOL.thy Thu Oct 30 09:15:54 2014 +0100 @@ -1692,8 +1692,11 @@ *} definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True" + lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl) +declare [[coercion_args NO_MATCH - -]] + simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct => let val thy = Proof_Context.theory_of ctxt