src/HOL/SMT.thy
changeset 58776 95e58e04e534
parent 58598 d9892c88cb56
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/SMT.thy	Fri Oct 24 15:07:49 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Fri Oct 24 15:07:51 2014 +0200
     1.3 @@ -322,6 +322,7 @@
     1.4    refl eq_commute conj_commute disj_commute simp_thms nnf_simps
     1.5    ring_distribs field_simps times_divide_eq_right times_divide_eq_left
     1.6    if_True if_False not_not
     1.7 +  NO_MATCH_def
     1.8  
     1.9  lemma [z3_rule]:
    1.10    "(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))"