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 1) (+ uf_1 (+ (* 2 (mod uf_1 2)) 1)))) |
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 |
) |