equal
deleted
inserted
replaced
320 |
320 |
321 lemmas [z3_rule] = |
321 lemmas [z3_rule] = |
322 refl eq_commute conj_commute disj_commute simp_thms nnf_simps |
322 refl eq_commute conj_commute disj_commute simp_thms nnf_simps |
323 ring_distribs field_simps times_divide_eq_right times_divide_eq_left |
323 ring_distribs field_simps times_divide_eq_right times_divide_eq_left |
324 if_True if_False not_not |
324 if_True if_False not_not |
|
325 NO_MATCH_def |
325 |
326 |
326 lemma [z3_rule]: |
327 lemma [z3_rule]: |
327 "(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))" |
328 "(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))" |
328 "(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))" |
329 "(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))" |
329 "(\<not> P \<and> Q) = (\<not> (P \<or> \<not> Q))" |
330 "(\<not> P \<and> Q) = (\<not> (P \<or> \<not> Q))" |