--- a/etc/isar-keywords.el Thu Feb 13 11:37:00 2014 +0100
+++ b/etc/isar-keywords.el Thu Feb 13 11:54:14 2014 +0100
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + HOL-Auth + HOL-BNF_Examples + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
+;; Generated from HOL + HOL-Auth + HOL-BNF_Examples + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Predicate_Compile_Examples + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
@@ -296,6 +296,7 @@
"using"
"value"
"values"
+ "values_prolog"
"welcome"
"with"
"wrap_free_constructors"
@@ -456,6 +457,7 @@
"unused_thms"
"value"
"values"
+ "values_prolog"
"welcome"))
(defconst isar-keywords-theory-begin
--- a/src/HOL/Library/Code_Prolog.thy Thu Feb 13 11:37:00 2014 +0100
+++ b/src/HOL/Library/Code_Prolog.thy Thu Feb 13 11:54:14 2014 +0100
@@ -6,6 +6,7 @@
theory Code_Prolog
imports Main
+keywords "values_prolog" :: diag
begin
ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Feb 13 11:37:00 2014 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Feb 13 11:54:14 2014 +0100
@@ -18,11 +18,11 @@
replacing = [],
manual_reorder = []}) *}
-values "{(x, y, z). append x y z}"
+values_prolog "{(x, y, z). append x y z}"
-values 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}"
+values_prolog 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}"
-values 3 "{(x, y, z). append x y z}"
+values_prolog 3 "{(x, y, z). append x y z}"
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
@@ -32,7 +32,7 @@
replacing = [],
manual_reorder = []}) *}
-values "{(x, y, z). append x y z}"
+values_prolog "{(x, y, z). append x y z}"
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
@@ -100,7 +100,7 @@
where
"queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys"
-values 10 "{ys. queen_9 ys}"
+values_prolog 10 "{ys. queen_9 ys}"
section {* Example symbolic derivation *}
@@ -190,10 +190,10 @@
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"
-values "{e. ops8 e}"
-values "{e. divide10 e}"
-values "{e. log10 e}"
-values "{e. times10 e}"
+values_prolog "{e. ops8 e}"
+values_prolog "{e. divide10 e}"
+values_prolog "{e. log10 e}"
+values_prolog "{e. times10 e}"
section {* Example negation *}
@@ -211,13 +211,13 @@
replacing = [],
manual_reorder = []}) *}
-values 2 "{y. notB y}"
+values_prolog 2 "{y. notB y}"
inductive notAB :: "abc * abc \<Rightarrow> bool"
where
"y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
-values 5 "{y. notAB y}"
+values_prolog 5 "{y. notAB y}"
section {* Example prolog conform variable names *}
@@ -225,6 +225,6 @@
where
"equals y' y'"
-values 1 "{(y, z). equals y z}"
+values_prolog 1 "{(y, z). equals y z}"
end
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Thu Feb 13 11:37:00 2014 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Thu Feb 13 11:54:14 2014 +0100
@@ -79,7 +79,7 @@
replacing = [],
manual_reorder = []}) *}
-values 40 "{s. hotel s}"
+values_prolog 40 "{s. hotel s}"
setup {*
Context.theory_map
--- a/src/HOL/ROOT Thu Feb 13 11:37:00 2014 +0100
+++ b/src/HOL/ROOT Thu Feb 13 11:54:14 2014 +0100
@@ -39,7 +39,7 @@
AList_Mapping
Code_Binary_Nat
Code_Char
- (* Code_Prolog FIXME cf. 76965c356d2a *)
+ Code_Prolog
Code_Real_Approx_By_Float
Code_Target_Numeral
DAList
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Feb 13 11:37:00 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Feb 13 11:54:14 2014 +0100
@@ -1042,17 +1042,16 @@
end |> Pretty.writeln
-(* renewing the values command for Prolog queries *)
+(* values command for Prolog queries *)
val opt_print_modes =
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
val _ =
- Outer_Syntax.improper_command @{command_spec "values"}
+ Outer_Syntax.improper_command @{command_spec "values_prolog"}
"enumerate and print comprehensions"
(opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
- >> (fn ((print_modes, soln), t) => Toplevel.keep
- (values_cmd print_modes soln t))) (*FIXME does not preserve the previous functionality*)
+ >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
(* quickcheck generator *)