diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
| commit | 10df4ba0752eb23c76b9aa847e3ad116673a47b6 (patch) | |
| tree | f41eec3963b7a9d96c0ea85179227d88ae57f0f6 /proofs/signatures/th_base.plf | |
| parent | 8d140a28c76095e148acd64e47b5ca0a92ca09be (diff) | |
CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature. Add regressions.
Diffstat (limited to 'proofs/signatures/th_base.plf')
| -rwxr-xr-x | proofs/signatures/th_base.plf | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf index 977409b6a..9dd950b5b 100755 --- a/proofs/signatures/th_base.plf +++ b/proofs/signatures/th_base.plf @@ -23,6 +23,7 @@ ; inference rules : (declare trust (th_holds false)) ; temporary +(declare trust_f (! f formula (th_holds f))) ; temporary (declare refl (! s sort |