author | boehmes |
Thu, 05 Nov 2009 15:24:49 +0100 | |
changeset 33446 | 153a27370a42 |
permissions | -rw-r--r-- |
33446
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
1 |
(benchmark Isabelle |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
2 |
:extrafuns ( |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
3 |
(uf_1 Int) |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
4 |
) |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
5 |
:assumption (not (< (+ uf_1 (+ (mod uf_1 2) (mod uf_1 2))) (+ uf_1 3))) |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
6 |
:formula true |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
7 |
) |