--- a/src/HOL/Prolog/Func.thy Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/Prolog/Func.thy Mon Nov 20 21:23:12 2006 +0100
@@ -20,8 +20,8 @@
true :: tm
false :: tm
- "and" :: "tm => tm => tm" (infixr 999)
- "eq" :: "tm => tm => tm" (infixr 999)
+ "and" :: "tm => tm => tm" (infixr "and" 999)
+ eq :: "tm => tm => tm" (infixr "eq" 999)
Z :: tm ("Z")
S :: "tm => tm"
@@ -60,6 +60,16 @@
eval ( Z * M) Z..
eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
-ML {* use_legacy_bindings (the_context ()) *}
+
+lemmas prog_Func = eval
+
+lemma "eval ((S (S Z)) + (S Z)) ?X"
+ apply (prolog prog_Func)
+ done
+
+lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
+ (n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"
+ apply (prolog prog_Func)
+ done
end