src/HOL/Prolog/Func.ML
author oheimb
Tue Jun 11 16:43:17 2002 +0200 (2002-06-11)
changeset 13208 965f95a3abd9
parent 12486 0ed8bdd883e0
child 14981 e73f8140af78
permissions -rw-r--r--
added the usual file headers
oheimb@13208
     1
(* Title:    HOL/Prolog/Func.ML
oheimb@13208
     2
    ID:       $Id$
oheimb@13208
     3
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
oheimb@13208
     4
    License:  GPL (GNU GENERAL PUBLIC LICENSE)
oheimb@13208
     5
*)
oheimb@13208
     6
oheimb@9015
     7
open Func;
oheimb@9015
     8
oheimb@9015
     9
val prog_Func = prog_HOHH @ [eval];
wenzelm@12486
    10
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
oheimb@9015
    11
val p = ptac prog_Func 1;
oheimb@9015
    12
oheimb@9015
    13
pgoal "eval ((S (S Z)) + (S Z)) ?X";
oheimb@9015
    14
oheimb@9015
    15
pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
oheimb@9015
    16
			\(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
oheimb@9015
    17
oheimb@9015
    18