diff options
Diffstat (limited to 'proofs/signatures/th_int.plf')
| -rw-r--r-- | proofs/signatures/th_int.plf | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/proofs/signatures/th_int.plf b/proofs/signatures/th_int.plf deleted file mode 100644 index 9a0a2d63c..000000000 --- a/proofs/signatures/th_int.plf +++ /dev/null @@ -1,25 +0,0 @@ -(declare Int sort) - -(define arithpred_Int (! x (term Int) - (! y (term Int) - formula))) - -(declare >_Int arithpred_Int) -(declare >=_Int arithpred_Int) -(declare <_Int arithpred_Int) -(declare <=_Int arithpred_Int) - -(define arithterm_Int (! x (term Int) - (! y (term Int) - (term Int)))) - -(declare +_Int arithterm_Int) -(declare -_Int arithterm_Int) -(declare *_Int arithterm_Int) ; is * ok to use? -(declare /_Int arithterm_Int) ; is / ok to use? - -; a constant term -(declare a_int (! x mpz (term Int))) - -; unary negation -(declare u-_Int (! t (term Int) (term Int))) |