src/HOL/Prolog/Func.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 9015 8006e9009621
child 12486 0ed8bdd883e0
permissions -rw-r--r--
improved theory reference in comment
oheimb@9015
     1
open Func;
oheimb@9015
     2
oheimb@9015
     3
val prog_Func = prog_HOHH @ [eval];
oheimb@9015
     4
fun pgoal s = (case Goal s of _ => by(prolog_tac prog_Func));
oheimb@9015
     5
val p = ptac prog_Func 1;
oheimb@9015
     6
oheimb@9015
     7
pgoal "eval ((S (S Z)) + (S Z)) ?X";
oheimb@9015
     8
oheimb@9015
     9
pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
oheimb@9015
    10
			\(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
oheimb@9015
    11
oheimb@9015
    12