equal
deleted
inserted
replaced
418 "(if P then \<not>Q else R) \<or> \<not>P \<or> Q" |
418 "(if P then \<not>Q else R) \<or> \<not>P \<or> Q" |
419 "(if P then Q else \<not>R) \<or> P \<or> R" |
419 "(if P then Q else \<not>R) \<or> P \<or> R" |
420 by auto |
420 by auto |
421 |
421 |
422 ML_file "Old_SMT/old_smt_real.ML" |
422 ML_file "Old_SMT/old_smt_real.ML" |
423 setup Old_SMT_Real.setup |
|
424 |
|
425 ML_file "Old_SMT/old_smt_word.ML" |
423 ML_file "Old_SMT/old_smt_word.ML" |
426 setup Old_SMT_Word.setup |
|
427 |
424 |
428 hide_type (open) pattern |
425 hide_type (open) pattern |
429 hide_const fun_app term_true term_false z3div z3mod |
426 hide_const fun_app term_true term_false z3div z3mod |
430 hide_const (open) trigger pat nopat weight |
427 hide_const (open) trigger pat nopat weight |
431 |
428 |