isabelle: src/HOL/Prolog/Func.ML@3d80209e9a53 (annotated)

13208 965f95a3abd9 added the usual file headers oheimb parents: 12486 diff changeset	1	(* Title: HOL/Prolog/Func.ML
965f95a3abd9 added the usual file headers oheimb parents: 12486 diff changeset	2	ID: $Id$
965f95a3abd9 added the usual file headers oheimb parents: 12486 diff changeset	3	Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
965f95a3abd9 added the usual file headers oheimb parents: 12486 diff changeset	4	*)
965f95a3abd9 added the usual file headers oheimb parents: 12486 diff changeset	5
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	6	open Func;
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	7
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	8	val prog_Func = prog_HOHH @ [eval];
12486 0ed8bdd883e0 isatool expandshort; wenzelm parents: 9015 diff changeset	9	fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	10	val p = ptac prog_Func 1;
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	11
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	12	pgoal "eval ((S (S Z)) + (S Z)) ?X";
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	13
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	14	pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	15	\(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	16
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	17

author	wenzelm
	Mon, 29 Aug 2005 16:18:04 +0200
changeset 17184	3d80209e9a53
parent 14981	e73f8140af78
child 17311	5b1d47d920ce
permissions	-rw-r--r--