# HG changeset patch
# User blanchet
# Date 1325611998 -3600
# Node ID eb85282db54e5fde370613384b22ca6438e13821
# Parent  1e35730bd8690ac5d2c33dcb45364cf840b8730f
no abuse of notation

diff -r 1e35730bd869 -r eb85282db54e src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Jan 03 18:33:18 2012 +0100
@@ -17,8 +17,7 @@
 
 chapter {* 2. First Steps *}
 
-nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
-                timeout = 240]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 subsection {* 2.1. Propositional Logic *}
 
@@ -31,23 +30,23 @@
 
 subsection {* 2.2. Type Variables *}
 
-lemma "P x \<Longrightarrow> P (THE y. P y)"
+lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [verbose, expect = genuine]
 oops
 
 subsection {* 2.3. Constants *}
 
-lemma "P x \<Longrightarrow> P (THE y. P y)"
+lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [show_consts, expect = genuine]
 nitpick [dont_specialize, show_consts, expect = genuine]
 oops
 
-lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
+lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [expect = none]
 nitpick [card 'a = 1\<emdash>50, expect = none]
 (* sledgehammer *)
-apply (metis the_equality)
-done
+sledgehammer
+by (metis the_equality)
 
 subsection {* 2.4. Skolemization *}
 
@@ -67,6 +66,7 @@
 
 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
 nitpick [expect = genuine]
+nitpick [binary_ints, bits = 16, expect = genuine]
 oops
 
 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
@@ -95,15 +95,14 @@
 
 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
 
-definition "three = {0\<Colon>nat, 1, 2}"
-typedef (open) three = three
-unfolding three_def by blast
+typedef three = "{0\<Colon>nat, 1, 2}"
+by blast
 
 definition A :: three where "A \<equiv> Abs_three 0"
 definition B :: three where "B \<equiv> Abs_three 1"
 definition C :: three where "C \<equiv> Abs_three 2"
 
-lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
+lemma "\<lbrakk>A \<in> X; B \<in> X\<rbrakk> \<Longrightarrow> c \<in> X"
 nitpick [show_datatypes, expect = genuine]
 oops
 
diff -r 1e35730bd869 -r eb85282db54e src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -836,11 +836,9 @@
 
 fun assign_operator_for_const (s, T) =
   if String.isPrefix ubfp_prefix s then
-    if is_fun_type T then xsym "\<subseteq>" "<=" ()
-    else xsym "\<le>" "<=" ()
+    xsym "\<le>" "<=" ()
   else if String.isPrefix lbfp_prefix s then
-    if is_fun_type T then xsym "\<supseteq>" ">=" ()
-    else xsym "\<ge>" ">=" ()
+    xsym "\<ge>" ">=" ()
   else if original_name s <> s then
     assign_operator_for_const (strip_first_name_sep s |> snd, T)
   else