src/HOL/Prolog/Func.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 13208 965f95a3abd9
child 17311 5b1d47d920ce
permissions -rw-r--r--
Merged in license change from Isabelle2004
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
*)
oheimb@13208
     5
oheimb@9015
     6
open Func;
oheimb@9015
     7
oheimb@9015
     8
val prog_Func = prog_HOHH @ [eval];
wenzelm@12486
     9
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
oheimb@9015
    10
val p = ptac prog_Func 1;
oheimb@9015
    11
oheimb@9015
    12
pgoal "eval ((S (S Z)) + (S Z)) ?X";
oheimb@9015
    13
oheimb@9015
    14
pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
oheimb@9015
    15
			\(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
oheimb@9015
    16
oheimb@9015
    17