src/HOL/Prolog/Func.ML
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14981 e73f8140af78
child 17311 5b1d47d920ce
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
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