diff options
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 |