summaryrefslogtreecommitdiff
path: root/proofs/signatures/smt.plf
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/signatures/smt.plf')
-rwxr-xr-xproofs/signatures/smt.plf3
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index bbee2d49b..942e17df0 100755
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -104,6 +104,9 @@
(! r2 (th_holds (not f))
(th_holds false)))))
+; truth
+(declare truth (th_holds true))
+
;; not not
(declare not_not_intro
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback