src/HOL/Prolog/Func.ML
changeset 21425 c11ab38b78a7
parent 21424 5295ffa18285
child 21426 87ac12bed1ab
     1.1 --- a/src/HOL/Prolog/Func.ML	Mon Nov 20 11:51:10 2006 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,13 +0,0 @@
     1.4 -(* Title:    HOL/Prolog/Func.ML
     1.5 -    ID:       $Id$
     1.6 -    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     1.7 -*)
     1.8 -
     1.9 -val prog_Func = prog_HOHH @ [eval];
    1.10 -fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
    1.11 -val p = ptac prog_Func 1;
    1.12 -
    1.13 -pgoal "eval ((S (S Z)) + (S Z)) ?X";
    1.14 -
    1.15 -pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
    1.16 -                        \(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";