do not redefine outer syntax commands;
authorwenzelm
Thu Feb 13 11:54:14 2014 +0100 (2014-02-13)
changeset 55447aa41ecbdc205
parent 55446 e77f2858bd59
child 55448 e42a3fc18458
do not redefine outer syntax commands;
etc/isar-keywords.el
src/HOL/Library/Code_Prolog.thy
src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
src/HOL/ROOT
src/HOL/Tools/Predicate_Compile/code_prolog.ML
     1.1 --- a/etc/isar-keywords.el	Thu Feb 13 11:37:00 2014 +0100
     1.2 +++ b/etc/isar-keywords.el	Thu Feb 13 11:54:14 2014 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  ;;
     1.5  ;; Keyword classification tables for Isabelle/Isar.
     1.6 -;; 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.
     1.7 +;; 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.
     1.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     1.9  ;;
    1.10  
    1.11 @@ -296,6 +296,7 @@
    1.12      "using"
    1.13      "value"
    1.14      "values"
    1.15 +    "values_prolog"
    1.16      "welcome"
    1.17      "with"
    1.18      "wrap_free_constructors"
    1.19 @@ -456,6 +457,7 @@
    1.20      "unused_thms"
    1.21      "value"
    1.22      "values"
    1.23 +    "values_prolog"
    1.24      "welcome"))
    1.25  
    1.26  (defconst isar-keywords-theory-begin
     2.1 --- a/src/HOL/Library/Code_Prolog.thy	Thu Feb 13 11:37:00 2014 +0100
     2.2 +++ b/src/HOL/Library/Code_Prolog.thy	Thu Feb 13 11:54:14 2014 +0100
     2.3 @@ -6,6 +6,7 @@
     2.4  
     2.5  theory Code_Prolog
     2.6  imports Main
     2.7 +keywords "values_prolog" :: diag
     2.8  begin
     2.9  
    2.10  ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Feb 13 11:37:00 2014 +0100
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Feb 13 11:54:14 2014 +0100
     3.3 @@ -18,11 +18,11 @@
     3.4     replacing = [],
     3.5     manual_reorder = []}) *}
     3.6  
     3.7 -values "{(x, y, z). append x y z}"
     3.8 +values_prolog "{(x, y, z). append x y z}"
     3.9  
    3.10 -values 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}"
    3.11 +values_prolog 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}"
    3.12  
    3.13 -values 3 "{(x, y, z). append x y z}"
    3.14 +values_prolog 3 "{(x, y, z). append x y z}"
    3.15  
    3.16  setup {* Code_Prolog.map_code_options (K
    3.17    {ensure_groundness = false,
    3.18 @@ -32,7 +32,7 @@
    3.19     replacing = [],
    3.20     manual_reorder = []}) *}
    3.21  
    3.22 -values "{(x, y, z). append x y z}"
    3.23 +values_prolog "{(x, y, z). append x y z}"
    3.24  
    3.25  setup {* Code_Prolog.map_code_options (K
    3.26    {ensure_groundness = false,
    3.27 @@ -100,7 +100,7 @@
    3.28  where
    3.29    "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys"
    3.30  
    3.31 -values 10 "{ys. queen_9 ys}"
    3.32 +values_prolog 10 "{ys. queen_9 ys}"
    3.33  
    3.34  
    3.35  section {* Example symbolic derivation *}
    3.36 @@ -190,10 +190,10 @@
    3.37  where
    3.38    "d (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult x x) x) x) x) x) x) x) x) x) x e ==> times10 e"
    3.39  
    3.40 -values "{e. ops8 e}"
    3.41 -values "{e. divide10 e}"
    3.42 -values "{e. log10 e}"
    3.43 -values "{e. times10 e}"
    3.44 +values_prolog "{e. ops8 e}"
    3.45 +values_prolog "{e. divide10 e}"
    3.46 +values_prolog "{e. log10 e}"
    3.47 +values_prolog "{e. times10 e}"
    3.48  
    3.49  section {* Example negation *}
    3.50  
    3.51 @@ -211,13 +211,13 @@
    3.52     replacing = [],
    3.53     manual_reorder = []}) *}
    3.54  
    3.55 -values 2 "{y. notB y}"
    3.56 +values_prolog 2 "{y. notB y}"
    3.57  
    3.58  inductive notAB :: "abc * abc \<Rightarrow> bool"
    3.59  where
    3.60    "y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
    3.61  
    3.62 -values 5 "{y. notAB y}"
    3.63 +values_prolog 5 "{y. notAB y}"
    3.64  
    3.65  section {* Example prolog conform variable names *}
    3.66  
    3.67 @@ -225,6 +225,6 @@
    3.68  where
    3.69    "equals y' y'"
    3.70  
    3.71 -values 1 "{(y, z). equals y z}"
    3.72 +values_prolog 1 "{(y, z). equals y z}"
    3.73  
    3.74  end
     4.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Thu Feb 13 11:37:00 2014 +0100
     4.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Thu Feb 13 11:54:14 2014 +0100
     4.3 @@ -79,7 +79,7 @@
     4.4    replacing = [],
     4.5    manual_reorder = []}) *}
     4.6  
     4.7 -values 40 "{s. hotel s}"
     4.8 +values_prolog 40 "{s. hotel s}"
     4.9  
    4.10  setup {*
    4.11    Context.theory_map
     5.1 --- a/src/HOL/ROOT	Thu Feb 13 11:37:00 2014 +0100
     5.2 +++ b/src/HOL/ROOT	Thu Feb 13 11:54:14 2014 +0100
     5.3 @@ -39,7 +39,7 @@
     5.4      AList_Mapping
     5.5      Code_Binary_Nat
     5.6      Code_Char
     5.7 -    (* Code_Prolog  FIXME cf. 76965c356d2a *)
     5.8 +    Code_Prolog
     5.9      Code_Real_Approx_By_Float
    5.10      Code_Target_Numeral
    5.11      DAList
     6.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 13 11:37:00 2014 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 13 11:54:14 2014 +0100
     6.3 @@ -1042,17 +1042,16 @@
     6.4    end |> Pretty.writeln
     6.5  
     6.6  
     6.7 -(* renewing the values command for Prolog queries *)
     6.8 +(* values command for Prolog queries *)
     6.9  
    6.10  val opt_print_modes =
    6.11    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
    6.12  
    6.13  val _ =
    6.14 -  Outer_Syntax.improper_command @{command_spec "values"}
    6.15 +  Outer_Syntax.improper_command @{command_spec "values_prolog"}
    6.16      "enumerate and print comprehensions"
    6.17      (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
    6.18 -     >> (fn ((print_modes, soln), t) => Toplevel.keep
    6.19 -          (values_cmd print_modes soln t))) (*FIXME does not preserve the previous functionality*)
    6.20 +     >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
    6.21  
    6.22  
    6.23  (* quickcheck generator *)