src/HOL/Prolog/Func.ML

added type global_theory -- theory or local_theory;
added begin/exit_local_theory;
removed theory_context;
renamed body_context_node to presentation_context;
removed copy (checkpoint twice instead -- avoids unrelated theories);

(* Title:    HOL/Prolog/Func.ML
    ID:       $Id$
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)

val prog_Func = prog_HOHH @ [eval];
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
val p = ptac prog_Func 1;

pgoal "eval ((S (S Z)) + (S Z)) ?X";

pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
                        \(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";