| author | wenzelm |
| Fri, 08 Mar 2002 16:24:06 +0100 | |
| changeset 13049 | ce180e5b7fa0 |
| parent 12486 | 0ed8bdd883e0 |
| child 13208 | 965f95a3abd9 |
| permissions | -rw-r--r-- |
| 9015 | 1 |
open Func; |
2 |
||
3 |
val prog_Func = prog_HOHH @ [eval]; |
|
| 12486 | 4 |
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func)); |
| 9015 | 5 |
val p = ptac prog_Func 1; |
6 |
||
7 |
pgoal "eval ((S (S Z)) + (S Z)) ?X"; |
|
8 |
||
9 |
pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \ |
|
10 |
\(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"; |
|
11 |
||
12 |