equal
deleted
inserted
replaced
16 |
16 |
17 text {* \medskip Late clause setup: installs \emph{all} simprules and |
17 text {* \medskip Late clause setup: installs \emph{all} simprules and |
18 claset rules into the clause cache; cf.\ theory @{text |
18 claset rules into the clause cache; cf.\ theory @{text |
19 Reconstruction}. *} |
19 Reconstruction}. *} |
20 |
20 |
|
21 declare subset_refl [intro] |
|
22 text {*Ensures that this important theorem is not superseded by the |
|
23 simplifier's "== True" version.*} |
21 setup ResAxioms.clause_setup |
24 setup ResAxioms.clause_setup |
|
25 declare subset_refl [rule del] |
|
26 text {*Removed again because it harms blast's performance.*} |
22 |
27 |
23 end |
28 end |