src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
 changeset 38731 2c8a595af43e parent 38728 182b180e9804 child 38735 cb9031a9dccf
```     1.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Aug 25 16:59:49 2010 +0200
1.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Aug 25 16:59:50 2010 +0200
1.3 @@ -9,8 +9,6 @@
1.4    "append [] ys ys"
1.5  | "append xs ys zs ==> append (x # xs) ys (x # zs)"
1.6
1.7 -code_pred append .
1.8 -
1.9  values 3 "{(x, y, z). append x y z}"
1.10
1.11
1.12 @@ -71,9 +69,7 @@
1.13  where
1.14    "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys"
1.15
1.16 -code_pred queen_9 .
1.17 -
1.18 -values 150 "{ys. queen_9 ys}"
1.19 +values 10 "{ys. queen_9 ys}"
1.20
1.21
1.22  section {* Example symbolic derivation *}
1.23 @@ -163,11 +159,6 @@
1.24  where
1.25    "d (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult x x) x) x) x) x) x) x) x) x) x e ==> times10 e"
1.26
1.27 -code_pred ops8 .
1.28 -code_pred divide10 .
1.29 -code_pred log10 .
1.30 -code_pred times10 .
1.31 -
1.32  values "{e. ops8 e}"
1.33  values "{e. divide10 e}"
1.34  values "{e. log10 e}"
1.35 @@ -181,8 +172,6 @@
1.36  where
1.37    "y \<noteq> B \<Longrightarrow> notB y"
1.38
1.39 -code_pred notB .
1.40 -
1.41  ML {* Code_Prolog.options := {ensure_groundness = true} *}
1.42
1.43  values 2 "{y. notB y}"
1.44 @@ -191,8 +180,6 @@
1.45  where
1.46    "y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
1.47
1.48 -code_pred notAB .
1.49 -
1.50  values 5 "{y. notAB y}"
1.51
1.52  end
```