equal
deleted
inserted
replaced
423 "(if P then \<not>Q else R) \<or> \<not>P \<or> Q" |
423 "(if P then \<not>Q else R) \<or> \<not>P \<or> Q" |
424 "(if P then Q else \<not>R) \<or> P \<or> R" |
424 "(if P then Q else \<not>R) \<or> P \<or> R" |
425 by auto |
425 by auto |
426 |
426 |
427 |
427 |
428 |
|
429 hide_type (open) pattern |
428 hide_type (open) pattern |
430 hide_const Pattern fun_app term_true term_false z3div z3mod |
429 hide_const Pattern fun_app term_true term_false z3div z3mod |
431 hide_const (open) trigger pat nopat weight |
430 hide_const (open) trigger pat nopat weight |
432 |
431 |
433 end |
432 end |