diff -r 5bbdd9a9df62 -r 2c8a595af43e src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Wed Aug 25 16:59:49 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Wed Aug 25 16:59:50 2010 +0200 @@ -9,8 +9,6 @@ "append [] ys ys" | "append xs ys zs ==> append (x # xs) ys (x # zs)" -code_pred append . - values 3 "{(x, y, z). append x y z}" @@ -71,9 +69,7 @@ where "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys" -code_pred queen_9 . - -values 150 "{ys. queen_9 ys}" +values 10 "{ys. queen_9 ys}" section {* Example symbolic derivation *} @@ -163,11 +159,6 @@ where "d (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult x x) x) x) x) x) x) x) x) x) x e ==> times10 e" -code_pred ops8 . -code_pred divide10 . -code_pred log10 . -code_pred times10 . - values "{e. ops8 e}" values "{e. divide10 e}" values "{e. log10 e}" @@ -181,8 +172,6 @@ where "y \ B \ notB y" -code_pred notB . - ML {* Code_Prolog.options := {ensure_groundness = true} *} values 2 "{y. notB y}" @@ -191,8 +180,6 @@ where "y \ A \ z \ B \ notAB (y, z)" -code_pred notAB . - values 5 "{y. notAB y}" end