tuning
authorblanchet
Thu, 16 Sep 2010 14:24:03 +0200
changeset 39456 37f1a961a918
parent 39455 c6b21584f336
child 39457 b505208f435d
tuning
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Thu Sep 16 13:52:17 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Thu Sep 16 14:24:03 2010 +0200
@@ -2,7 +2,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2008, 2009, 2010
 
-ML interface on top of Kodkod.
+ML interface for Kodkod.
 *)
 
 signature KODKOD =
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Sep 16 13:52:17 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Sep 16 14:24:03 2010 +0200
@@ -1019,7 +1019,7 @@
 fun kodkod_formula_from_nut ofs
         (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
                 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
-                kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
+                kk_lone, kk_some, kk_rel_let, kk_rel_if, kk_union,
                 kk_difference, kk_intersect, kk_product, kk_join, kk_closure,
                 kk_comprehension, kk_project, kk_project_seq, kk_not3,
                 kk_nat_less, kk_int_less, ...}) u =