author | wenzelm |
Wed, 07 Sep 2005 21:07:09 +0200 | |
changeset 17311 | 5b1d47d920ce |
parent 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
13208 | 1 |
(* Title: HOL/Prolog/Func.ML |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) |
|
4 |
*) |
|
5 |
||
9015 | 6 |
val prog_Func = prog_HOHH @ [eval]; |
12486 | 7 |
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func)); |
9015 | 8 |
val p = ptac prog_Func 1; |
9 |
||
10 |
pgoal "eval ((S (S Z)) + (S Z)) ?X"; |
|
11 |
||
12 |
pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \ |
|
17311 | 13 |
\(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"; |