src/HOL/HOL.thy
changeset 59779 b6bda9140e39
parent 59628 2b15625b85fc
child 59864 c777743294e1
     1.1 --- a/src/HOL/HOL.thy	Mon Mar 23 10:16:20 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Mar 23 15:08:02 2015 +0100
     1.3 @@ -1671,13 +1671,13 @@
     1.4   The simplification procedure can be used to avoid simplification of terms of a certain form
     1.5  *}
     1.6  
     1.7 -definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"
     1.8 +definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH pat val \<equiv> True"
     1.9  
    1.10 -lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)
    1.11 +lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" by (rule refl)
    1.12  
    1.13  declare [[coercion_args NO_MATCH - -]]
    1.14  
    1.15 -simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>
    1.16 +simproc_setup NO_MATCH ("NO_MATCH pat val") = {* fn _ => fn ctxt => fn ct =>
    1.17    let
    1.18      val thy = Proof_Context.theory_of ctxt
    1.19      val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
    1.20 @@ -1686,7 +1686,7 @@
    1.21  *}
    1.22  
    1.23  text {*
    1.24 -  This setup ensures that a rewrite rule of the form @{term "NO_MATCH val pat \<Longrightarrow> t"}
    1.25 +  This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \<Longrightarrow> t"}
    1.26    is only applied, if the pattern @{term pat} does not match the value @{term val}.
    1.27  *}
    1.28