--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Aug 31 15:07:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Aug 31 15:21:56 2010 +0200
@@ -10,8 +10,12 @@
"append [] ys ys"
| "append xs ys zs ==> append (x # xs) ys (x # zs)"
-setup {* Code_Prolog.map_code_options (K {ensure_groundness = false,
- limited_types = [], limited_predicates = [], replacing = [],
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = false,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
prolog_system = Code_Prolog.SWI_PROLOG}) *}
values "{(x, y, z). append x y z}"
@@ -20,14 +24,20 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
- limited_types = [], limited_predicates = [], replacing = [],
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
prolog_system = Code_Prolog.YAP}) *}
values "{(x, y, z). append x y z}"
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
- limited_types = [], limited_predicates = [], replacing = [],
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
prolog_system = Code_Prolog.SWI_PROLOG}) *}
@@ -191,11 +201,13 @@
where
"y \<noteq> B \<Longrightarrow> notB y"
-setup {* Code_Prolog.map_code_options (K {ensure_groundness = true,
- limited_types = [],
- limited_predicates = [],
- replacing = [],
- prolog_system = Code_Prolog.SWI_PROLOG}) *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
values 2 "{y. notB y}"