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