1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue May 24 00:01:33 2011 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue May 24 00:01:33 2011 +0200
     1.3 @@ -346,7 +346,7 @@
     1.4  \prew
     1.5  \textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
     1.6  can be entered as \texttt{-} (hyphen) or
     1.7 -\texttt{\char`\\\char`\<midarrow\char`\>}.} \\[2\smallskipamount]
     1.8 +\texttt{\char`\\\char`\<emdash\char`\>}.} \\[2\smallskipamount]
     1.9  \slshape Nitpick found no counterexample.
    1.10  \postw
    1.11  
    1.12 @@ -1890,7 +1890,7 @@
    1.13  \item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
    1.14  \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
    1.15  \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
    1.16 -of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
    1.17 +of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<emdash\char`\>}.
    1.18  \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
    1.19  \item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
    1.20  (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}

     2.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue May 24 00:01:33 2011 +0200
     2.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue May 24 00:01:33 2011 +0200
     2.3 @@ -11,29 +11,29 @@
     2.4  imports Main
     2.5  begin
     2.6  
     2.7 -nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0,
     2.8 +nitpick_params [verbose, card = 1\<emdash>6, unary_ints, max_potential = 0,
     2.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    2.10  
    2.11  subsection {* Curry in a Hurry *}
    2.12  
    2.13  lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
    2.14 -nitpick [card = 1\<midarrow>12, expect = none]
    2.15 +nitpick [card = 1\<emdash>12, expect = none]
    2.16  by auto
    2.17  
    2.18  lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
    2.19 -nitpick [card = 1\<midarrow>12, expect = none]
    2.20 +nitpick [card = 1\<emdash>12, expect = none]
    2.21  by auto
    2.22  
    2.23  lemma "split (curry f) = f"
    2.24 -nitpick [card = 1\<midarrow>12, expect = none]
    2.25 +nitpick [card = 1\<emdash>12, expect = none]
    2.26  by auto
    2.27  
    2.28  lemma "curry (split f) = f"
    2.29 -nitpick [card = 1\<midarrow>12, expect = none]
    2.30 +nitpick [card = 1\<emdash>12, expect = none]
    2.31  by auto
    2.32  
    2.33  lemma "split (\<lambda>x y. f (x, y)) = f"
    2.34 -nitpick [card = 1\<midarrow>12, expect = none]
    2.35 +nitpick [card = 1\<emdash>12, expect = none]
    2.36  by auto
    2.37  
    2.38  subsection {* Representations *}
    2.39 @@ -44,7 +44,7 @@
    2.40  
    2.41  lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
    2.42  nitpick [card 'a = 25, card 'b = 24, expect = genuine]
    2.43 -nitpick [card = 1\<midarrow>10, mono, expect = none]
    2.44 +nitpick [card = 1\<emdash>10, mono, expect = none]
    2.45  oops
    2.46  
    2.47  lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
    2.48 @@ -56,39 +56,39 @@
    2.49  oops
    2.50  
    2.51  lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
    2.52 -nitpick [card = 1\<midarrow>12, expect = none]
    2.53 +nitpick [card = 1\<emdash>12, expect = none]
    2.54  by auto
    2.55  
    2.56  lemma "fst (a, b) = a"
    2.57 -nitpick [card = 1\<midarrow>20, expect = none]
    2.58 +nitpick [card = 1\<emdash>20, expect = none]
    2.59  by auto
    2.60  
    2.61  lemma "\<exists>P. P = Id"
    2.62 -nitpick [card = 1\<midarrow>20, expect = none]
    2.63 +nitpick [card = 1\<emdash>20, expect = none]
    2.64  by auto
    2.65  
    2.66  lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
    2.67 -nitpick [card = 1\<midarrow>3, expect = none]
    2.68 +nitpick [card = 1\<emdash>3, expect = none]
    2.69  by auto
    2.70  
    2.71  lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
    2.72 -nitpick [card = 1\<midarrow>4, expect = none]
    2.73 +nitpick [card = 1\<emdash>4, expect = none]
    2.74  by auto
    2.75  
    2.76  lemma "Id (a, a)"
    2.77 -nitpick [card = 1\<midarrow>50, expect = none]
    2.78 +nitpick [card = 1\<emdash>50, expect = none]
    2.79  by (auto simp: Id_def Collect_def)
    2.80  
    2.81  lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
    2.82 -nitpick [card = 1\<midarrow>10, expect = none]
    2.83 +nitpick [card = 1\<emdash>10, expect = none]
    2.84  by (auto simp: Id_def Collect_def)
    2.85  
    2.86  lemma "UNIV (x\<Colon>'a\<times>'a)"
    2.87 -nitpick [card = 1\<midarrow>50, expect = none]
    2.88 +nitpick [card = 1\<emdash>50, expect = none]
    2.89  sorry
    2.90  
    2.91  lemma "{} = A - A"
    2.92 -nitpick [card = 1\<midarrow>100, expect = none]
    2.93 +nitpick [card = 1\<emdash>100, expect = none]
    2.94  by auto
    2.95  
    2.96  lemma "g = Let (A \<or> B)"
    2.97 @@ -132,7 +132,7 @@
    2.98  oops
    2.99  
   2.100  lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
   2.101 -nitpick [card = 1\<midarrow>10, expect = none]
   2.102 +nitpick [card = 1\<emdash>10, expect = none]
   2.103  by auto
   2.104  
   2.105  lemma "\<exists>F. F a b = G a b"
   2.106 @@ -149,7 +149,7 @@
   2.107  
   2.108  lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
   2.109         A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
   2.110 -nitpick [card = 1\<midarrow>25, expect = none]
   2.111 +nitpick [card = 1\<emdash>25, expect = none]
   2.112  by auto
   2.113  
   2.114  lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
   2.115 @@ -174,19 +174,19 @@
   2.116  oops
   2.117  
   2.118  lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
   2.119 -nitpick [card 'a = 1\<midarrow>15, expect = none]
   2.120 +nitpick [card 'a = 1\<emdash>15, expect = none]
   2.121  by auto
   2.122  
   2.123  lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
   2.124 -nitpick [card = 1\<midarrow>15, expect = none]
   2.125 +nitpick [card = 1\<emdash>15, expect = none]
   2.126  by auto
   2.127  
   2.128  lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
   2.129 -nitpick [card = 1\<midarrow>4, expect = none]
   2.130 +nitpick [card = 1\<emdash>4, expect = none]
   2.131  by auto
   2.132  
   2.133  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   2.134 -nitpick [card = 1\<midarrow>4, expect = none]
   2.135 +nitpick [card = 1\<emdash>4, expect = none]
   2.136  by auto
   2.137  
   2.138  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
   2.139 @@ -195,42 +195,42 @@
   2.140  
   2.141  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   2.142         f u v w x y z = f u (g u) w (h u w) y (k u w y)"
   2.143 -nitpick [card = 1\<midarrow>2, expect = none]
   2.144 +nitpick [card = 1\<emdash>2, expect = none]
   2.145  sorry
   2.146  
   2.147  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   2.148         f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
   2.149 -nitpick [card = 1\<midarrow>2, expect = genuine]
   2.150 +nitpick [card = 1\<emdash>2, expect = genuine]
   2.151  oops
   2.152  
   2.153  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   2.154         f u v w x y z = f u (g u w) w (h u w) y (k u w y)"
   2.155 -nitpick [card = 1\<midarrow>2, expect = genuine]
   2.156 +nitpick [card = 1\<emdash>2, expect = genuine]
   2.157  oops
   2.158  
   2.159  lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
   2.160         f u v w x = f u (g u) w (h u w)"
   2.161 -nitpick [card = 1\<midarrow>2, expect = none]
   2.162 +nitpick [card = 1\<emdash>2, expect = none]
   2.163  sorry
   2.164  
   2.165  lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
   2.166         f u v w x = f u (g u w) w (h u)"
   2.167 -nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
   2.168 +nitpick [card = 1\<emdash>2, dont_box, expect = genuine]
   2.169  oops
   2.170  
   2.171  lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
   2.172         f u v w x = f u (g u) w (h u w)"
   2.173 -nitpick [card = 1\<midarrow>2, dont_box, expect = none]
   2.174 +nitpick [card = 1\<emdash>2, dont_box, expect = none]
   2.175  sorry
   2.176  
   2.177  lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
   2.178         f u v w x = f u (g u w) w (h u)"
   2.179 -nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
   2.180 +nitpick [card = 1\<emdash>2, dont_box, expect = genuine]
   2.181  oops
   2.182  
   2.183  lemma "\<forall>x. if (\<forall>y. x = y) then False else True"
   2.184  nitpick [card = 1, expect = genuine]
   2.185 -nitpick [card = 2\<midarrow>5, expect = none]
   2.186 +nitpick [card = 2\<emdash>5, expect = none]
   2.187  oops
   2.188  
   2.189  lemma "\<forall>x\<Colon>'a\<times>'b. if (\<forall>y. x = y) then False else True"
   2.190 @@ -323,15 +323,15 @@
   2.191  oops
   2.192  
   2.193  lemma "P x \<equiv> P x"
   2.194 -nitpick [card = 1\<midarrow>10, expect = none]
   2.195 +nitpick [card = 1\<emdash>10, expect = none]
   2.196  by auto
   2.197  
   2.198  lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x"
   2.199 -nitpick [card = 1\<midarrow>10, expect = none]
   2.200 +nitpick [card = 1\<emdash>10, expect = none]
   2.201  by auto
   2.202  
   2.203  lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x"
   2.204 -nitpick [card = 1\<midarrow>10, expect = none]
   2.205 +nitpick [card = 1\<emdash>10, expect = none]
   2.206  by auto
   2.207  
   2.208  lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False"
   2.209 @@ -343,7 +343,7 @@
   2.210  by auto
   2.211  
   2.212  lemma "P x \<Longrightarrow> P x"
   2.213 -nitpick [card = 1\<midarrow>10, expect = none]
   2.214 +nitpick [card = 1\<emdash>10, expect = none]
   2.215  by auto
   2.216  
   2.217  lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False"
   2.218 @@ -604,11 +604,11 @@
   2.219  by simp
   2.220  
   2.221  lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))"
   2.222 -nitpick [card = 1\<midarrow>2, expect = none]
   2.223 +nitpick [card = 1\<emdash>2, expect = none]
   2.224  by auto
   2.225  
   2.226  lemma "rtrancl = (\<lambda>x. rtrancl x \<union> {(y, y)})"
   2.227 -nitpick [card = 1\<midarrow>3, expect = none]
   2.228 +nitpick [card = 1\<emdash>3, expect = none]
   2.229  apply (rule ext)
   2.230  by auto
   2.231  
   2.232 @@ -617,11 +617,11 @@
   2.233  by auto
   2.234  
   2.235  lemma "((x, x), (x, x)) \<in> rtrancl {}"
   2.236 -nitpick [card = 1\<midarrow>5, expect = none]
   2.237 +nitpick [card = 1\<emdash>5, expect = none]
   2.238  by auto
   2.239  
   2.240  lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
   2.241 -nitpick [card = 1\<midarrow>5, expect = none]
   2.242 +nitpick [card = 1\<emdash>5, expect = none]
   2.243  by auto
   2.244  
   2.245  lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
   2.246 @@ -629,27 +629,27 @@
   2.247  by auto
   2.248  
   2.249  lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
   2.250 -nitpick [card = 1\<midarrow>5, expect = none]
   2.251 +nitpick [card = 1\<emdash>5, expect = none]
   2.252  by auto
   2.253  
   2.254  lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
   2.255 -nitpick [card = 1\<midarrow>5, expect = none]
   2.256 +nitpick [card = 1\<emdash>5, expect = none]
   2.257  by auto
   2.258  
   2.259  lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
   2.260 -nitpick [card = 1\<midarrow>5, expect = none]
   2.261 +nitpick [card = 1\<emdash>5, expect = none]
   2.262  by auto
   2.263  
   2.264  lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))"
   2.265 -nitpick [card = 1\<midarrow>5, expect = none]
   2.266 +nitpick [card = 1\<emdash>5, expect = none]
   2.267  by auto
   2.268  
   2.269  lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
   2.270 -nitpick [card = 1\<midarrow>5, expect = none]
   2.271 +nitpick [card = 1\<emdash>5, expect = none]
   2.272  by auto
   2.273  
   2.274  lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
   2.275 -nitpick [card = 1\<midarrow>5, expect = none]
   2.276 +nitpick [card = 1\<emdash>5, expect = none]
   2.277  by auto
   2.278  
   2.279  lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B"
   2.280 @@ -661,7 +661,7 @@
   2.281  by auto
   2.282  
   2.283  lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"
   2.284 -nitpick [card = 1\<midarrow>7, expect = none]
   2.285 +nitpick [card = 1\<emdash>7, expect = none]
   2.286  by auto
   2.287  
   2.288  lemma "A \<union> - A = UNIV"
   2.289 @@ -695,7 +695,7 @@
   2.290  oops
   2.291  
   2.292  lemma "\<exists>x. x = The"
   2.293 -nitpick [card = 1\<midarrow>3]
   2.294 +nitpick [card = 1\<emdash>3]
   2.295  by auto
   2.296  
   2.297  lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x"
   2.298 @@ -708,11 +708,11 @@
   2.299  
   2.300  lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = x \<or> The P = y"
   2.301  nitpick [card = 2, expect = none]
   2.302 -nitpick [card = 3\<midarrow>5, expect = genuine]
   2.303 +nitpick [card = 3\<emdash>5, expect = genuine]
   2.304  oops
   2.305  
   2.306  lemma "P x \<Longrightarrow> P (The P)"
   2.307 -nitpick [card = 1\<midarrow>2, expect = none]
   2.308 +nitpick [card = 1\<emdash>2, expect = none]
   2.309  nitpick [card = 8, expect = genuine]
   2.310  oops
   2.311  
   2.312 @@ -721,7 +721,7 @@
   2.313  oops
   2.314  
   2.315  lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))"
   2.316 -nitpick [card = 1\<midarrow>5, expect = none]
   2.317 +nitpick [card = 1\<emdash>5, expect = none]
   2.318  by auto
   2.319  
   2.320  lemma "x = Eps"
   2.321 @@ -729,7 +729,7 @@
   2.322  oops
   2.323  
   2.324  lemma "\<exists>x. x = Eps"
   2.325 -nitpick [card = 1\<midarrow>3, expect = none]
   2.326 +nitpick [card = 1\<emdash>3, expect = none]
   2.327  by auto
   2.328  
   2.329  lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x"
   2.330 @@ -742,7 +742,7 @@
   2.331  oops
   2.332  
   2.333  lemma "P x \<Longrightarrow> P (Eps P)"
   2.334 -nitpick [card = 1\<midarrow>8, expect = none]
   2.335 +nitpick [card = 1\<emdash>8, expect = none]
   2.336  by (metis exE_some)
   2.337  
   2.338  lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y"

     3.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Tue May 24 00:01:33 2011 +0200
     3.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Tue May 24 00:01:33 2011 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -nitpick_params [verbose, card = 1\<midarrow>8, max_potential = 0,
     3.8 +nitpick_params [verbose, card = 1\<emdash>8, max_potential = 0,
     3.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    3.10  
    3.11  primrec rot where
    3.12 @@ -23,7 +23,7 @@
    3.13  "rot NibbleF = Nibble0"
    3.14  
    3.15  lemma "rot n \<noteq> n"
    3.16 -nitpick [card = 1\<midarrow>8,16, verbose, expect = none]
    3.17 +nitpick [card = 1\<emdash>8,16, verbose, expect = none]
    3.18  sorry
    3.19  
    3.20  lemma "rot Nibble2 \<noteq> Nibble3"

     4.1 --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue May 24 00:01:33 2011 +0200
     4.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue May 24 00:01:33 2011 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 -nitpick_params [verbose, card = 1\<midarrow>8, unary_ints,
     4.8 +nitpick_params [verbose, card = 1\<emdash>8, unary_ints,
     4.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    4.10  
    4.11  inductive p1 :: "nat \<Rightarrow> bool" where

     5.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue May 24 00:01:33 2011 +0200
     5.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue May 24 00:01:33 2011 +0200
     5.3 @@ -11,7 +11,7 @@
     5.4  imports Nitpick
     5.5  begin
     5.6  
     5.7 -nitpick_params [verbose, card = 1\<midarrow>5, bits = 1,2,3,4,6,
     5.8 +nitpick_params [verbose, card = 1\<emdash>5, bits = 1,2,3,4,6,
     5.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    5.10  
    5.11  lemma "Suc x = x + 1"
    5.12 @@ -187,7 +187,7 @@
    5.13  
    5.14  lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)"
    5.15  nitpick [unary_ints, expect = none]
    5.16 -nitpick [binary_ints, card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
    5.17 +nitpick [binary_ints, card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
    5.18  sorry
    5.19  
    5.20  lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))"

     6.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue May 24 00:01:33 2011 +0200
     6.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue May 24 00:01:33 2011 +0200
     6.3 @@ -44,7 +44,7 @@
     6.4  
     6.5  lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
     6.6  nitpick [expect = none]
     6.7 -nitpick [card 'a = 1\<midarrow>50, expect = none]
     6.8 +nitpick [card 'a = 1\<emdash>50, expect = none]
     6.9  (* sledgehammer *)
    6.10  apply (metis the_equality)
    6.11  done
    6.12 @@ -227,7 +227,7 @@
    6.13  
    6.14  lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
    6.15  nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
    6.16 -nitpick [card = 1\<midarrow>5, expect = none]
    6.17 +nitpick [card = 1\<emdash>5, expect = none]
    6.18  sorry
    6.19  
    6.20  subsection {* 3.10. Boxing *}
    6.21 @@ -263,7 +263,7 @@
    6.22  "subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
    6.23  
    6.24  lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
    6.25 -nitpick [card = 1\<midarrow>5, expect = none]
    6.26 +nitpick [card = 1\<emdash>5, expect = none]
    6.27  sorry
    6.28  
    6.29  subsection {* 3.11. Scope Monotonicity *}
    6.30 @@ -288,7 +288,7 @@
    6.31  (* nitpick *)
    6.32  apply (induct set: reach)
    6.33    apply auto
    6.34 - nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
    6.35 + nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
    6.36   apply (thin_tac "n \<in> reach")
    6.37   nitpick [expect = genuine]
    6.38  oops
    6.39 @@ -297,7 +297,7 @@
    6.40  (* nitpick *)
    6.41  apply (induct set: reach)
    6.42    apply auto
    6.43 - nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
    6.44 + nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
    6.45   apply (thin_tac "n \<in> reach")
    6.46   nitpick [expect = genuine]
    6.47  oops
    6.48 @@ -336,7 +336,7 @@
    6.49    case Leaf thus ?case by simp
    6.50  next
    6.51    case (Branch t u) thus ?case
    6.52 -  nitpick [non_std, card = 1\<midarrow>4, expect = none]
    6.53 +  nitpick [non_std, card = 1\<emdash>4, expect = none]
    6.54    by auto
    6.55  qed
    6.56  
    6.57 @@ -384,7 +384,7 @@
    6.58  
    6.59  theorem S\<^isub>3_sound:
    6.60  "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    6.61 -nitpick [card = 1\<midarrow>5, expect = none]
    6.62 +nitpick [card = 1\<emdash>5, expect = none]
    6.63  sorry
    6.64  
    6.65  theorem S\<^isub>3_complete:
    6.66 @@ -403,19 +403,19 @@
    6.67  
    6.68  theorem S\<^isub>4_sound:
    6.69  "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    6.70 -nitpick [card = 1\<midarrow>5, expect = none]
    6.71 +nitpick [card = 1\<emdash>5, expect = none]
    6.72  sorry
    6.73  
    6.74  theorem S\<^isub>4_complete:
    6.75  "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
    6.76 -nitpick [card = 1\<midarrow>5, expect = none]
    6.77 +nitpick [card = 1\<emdash>5, expect = none]
    6.78  sorry
    6.79  
    6.80  theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
    6.81  "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    6.82  "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
    6.83  "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
    6.84 -nitpick [card = 1\<midarrow>5, expect = none]
    6.85 +nitpick [card = 1\<emdash>5, expect = none]
    6.86  sorry
    6.87  
    6.88  subsection {* 4.2. AA Trees *}
    6.89 @@ -469,13 +469,13 @@
    6.90  theorem dataset_skew_split:
    6.91  "dataset (skew t) = dataset t"
    6.92  "dataset (split t) = dataset t"
    6.93 -nitpick [card = 1\<midarrow>5, expect = none]
    6.94 +nitpick [card = 1\<emdash>5, expect = none]
    6.95  sorry
    6.96  
    6.97  theorem wf_skew_split:
    6.98  "wf t \<Longrightarrow> skew t = t"
    6.99  "wf t \<Longrightarrow> split t = t"
   6.100 -nitpick [card = 1\<midarrow>5, expect = none]
   6.101 +nitpick [card = 1\<emdash>5, expect = none]
   6.102  sorry
   6.103  
   6.104  primrec insort\<^isub>1 where
   6.105 @@ -499,11 +499,11 @@
   6.106                         (if x > y then insort\<^isub>2 u x else u))"
   6.107  
   6.108  theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
   6.109 -nitpick [card = 1\<midarrow>5, expect = none]
   6.110 +nitpick [card = 1\<emdash>5, expect = none]
   6.111  sorry
   6.112  
   6.113  theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
   6.114 -nitpick [card = 1\<midarrow>5, expect = none]
   6.115 +nitpick [card = 1\<emdash>5, expect = none]
   6.116  sorry
   6.117  
   6.118  end

     7.1 --- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Tue May 24 00:01:33 2011 +0200
     7.2 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Tue May 24 00:01:33 2011 +0200
     7.3 @@ -11,7 +11,7 @@
     7.4  imports Main
     7.5  begin
     7.6  
     7.7 -nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
     7.8 +nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
     7.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    7.10  
    7.11  record point2d =

     8.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue May 24 00:01:33 2011 +0200
     8.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue May 24 00:01:33 2011 +0200
     8.3 @@ -11,7 +11,7 @@
     8.4  imports Main
     8.5  begin
     8.6  
     8.7 -nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
     8.8 +nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
     8.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    8.10  
    8.11  lemma "P \<and> Q"
    8.12 @@ -283,7 +283,7 @@
    8.13  text {* ``Every point is a fixed point of some function.'' *}
    8.14  
    8.15  lemma "\<exists>f. f x = x"
    8.16 -nitpick [card = 1\<midarrow>7, expect = none]
    8.17 +nitpick [card = 1\<emdash>7, expect = none]
    8.18  apply (rule_tac x = "\<lambda>x. x" in exI)
    8.19  apply simp
    8.20  done
    8.21 @@ -745,7 +745,7 @@
    8.22  oops
    8.23  
    8.24  lemma "T3_rec e (E x) = e x"
    8.25 -nitpick [card = 1\<midarrow>4, expect = none]
    8.26 +nitpick [card = 1\<emdash>4, expect = none]
    8.27  apply simp
    8.28  done
    8.29  
    8.30 @@ -774,7 +774,7 @@
    8.31  oops
    8.32  
    8.33  lemma "P Suc"
    8.34 -nitpick [card = 1\<midarrow>7, expect = none]
    8.35 +nitpick [card = 1\<emdash>7, expect = none]
    8.36  oops
    8.37  
    8.38  lemma "nat_rec zero suc 0 = zero"
    8.39 @@ -810,12 +810,12 @@
    8.40  oops
    8.41  
    8.42  lemma "list_rec nil cons [] = nil"
    8.43 -nitpick [card = 1\<midarrow>5, expect = none]
    8.44 +nitpick [card = 1\<emdash>5, expect = none]
    8.45  apply simp
    8.46  done
    8.47  
    8.48  lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
    8.49 -nitpick [card = 1\<midarrow>5, expect = none]
    8.50 +nitpick [card = 1\<emdash>5, expect = none]
    8.51  apply simp
    8.52  done
    8.53  
    8.54 @@ -888,7 +888,7 @@
    8.55  done
    8.56  
    8.57  lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
    8.58 -nitpick [card = 1\<midarrow>5, expect = none]
    8.59 +nitpick [card = 1\<emdash>5, expect = none]
    8.60  apply simp
    8.61  done
    8.62  
    8.63 @@ -926,12 +926,12 @@
    8.64  oops
    8.65  
    8.66  lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
    8.67 -nitpick [card = 1\<midarrow>3, expect = none]
    8.68 +nitpick [card = 1\<emdash>3, expect = none]
    8.69  apply simp
    8.70  done
    8.71  
    8.72  lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"
    8.73 -nitpick [card = 1\<midarrow>3, expect = none]
    8.74 +nitpick [card = 1\<emdash>3, expect = none]
    8.75  apply simp
    8.76  done
    8.77  
    8.78 @@ -944,7 +944,7 @@
    8.79  oops
    8.80  
    8.81  lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"
    8.82 -nitpick [card = 1\<midarrow>3, expect = none]
    8.83 +nitpick [card = 1\<emdash>3, expect = none]
    8.84  apply simp
    8.85  done
    8.86  
    8.87 @@ -1004,32 +1004,32 @@
    8.88  oops
    8.89  
    8.90  lemma "X_Y_rec_1 a b c d e f A = a"
    8.91 -nitpick [card = 1\<midarrow>5, expect = none]
    8.92 +nitpick [card = 1\<emdash>5, expect = none]
    8.93  apply simp
    8.94  done
    8.95  
    8.96  lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"
    8.97 -nitpick [card = 1\<midarrow>5, expect = none]
    8.98 +nitpick [card = 1\<emdash>5, expect = none]
    8.99  apply simp
   8.100  done
   8.101  
   8.102  lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"
   8.103 -nitpick [card = 1\<midarrow>5, expect = none]
   8.104 +nitpick [card = 1\<emdash>5, expect = none]
   8.105  apply simp
   8.106  done
   8.107  
   8.108  lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"
   8.109 -nitpick [card = 1\<midarrow>5, expect = none]
   8.110 +nitpick [card = 1\<emdash>5, expect = none]
   8.111  apply simp
   8.112  done
   8.113  
   8.114  lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"
   8.115 -nitpick [card = 1\<midarrow>5, expect = none]
   8.116 +nitpick [card = 1\<emdash>5, expect = none]
   8.117  apply simp
   8.118  done
   8.119  
   8.120  lemma "X_Y_rec_2 a b c d e f F = f"
   8.121 -nitpick [card = 1\<midarrow>5, expect = none]
   8.122 +nitpick [card = 1\<emdash>5, expect = none]
   8.123  apply simp
   8.124  done
   8.125  
   8.126 @@ -1060,32 +1060,32 @@
   8.127  oops
   8.128  
   8.129  lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
   8.130 -nitpick [card = 1\<midarrow>5, expect = none]
   8.131 +nitpick [card = 1\<emdash>5, expect = none]
   8.132  apply simp
   8.133  done
   8.134  
   8.135  lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"
   8.136 -nitpick [card = 1\<midarrow>3, expect = none]
   8.137 +nitpick [card = 1\<emdash>3, expect = none]
   8.138  apply simp
   8.139  done
   8.140  
   8.141  lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
   8.142 -nitpick [card = 1\<midarrow>4, expect = none]
   8.143 +nitpick [card = 1\<emdash>4, expect = none]
   8.144  apply simp
   8.145  done
   8.146  
   8.147  lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
   8.148 -nitpick [card = 1\<midarrow>4, expect = none]
   8.149 +nitpick [card = 1\<emdash>4, expect = none]
   8.150  apply simp
   8.151  done
   8.152  
   8.153  lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
   8.154 -nitpick [card = 1\<midarrow>4, expect = none]
   8.155 +nitpick [card = 1\<emdash>4, expect = none]
   8.156  apply simp
   8.157  done
   8.158  
   8.159  lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
   8.160 -nitpick [card = 1\<midarrow>4, expect = none]
   8.161 +nitpick [card = 1\<emdash>4, expect = none]
   8.162  apply simp
   8.163  done
   8.164  
   8.165 @@ -1116,17 +1116,17 @@
   8.166  oops
   8.167  
   8.168  lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
   8.169 -nitpick [card = 1\<midarrow>2, expect = none]
   8.170 +nitpick [card = 1\<emdash>2, expect = none]
   8.171  apply simp
   8.172  done
   8.173  
   8.174  lemma "YOpt_rec_2 cy n s None = n"
   8.175 -nitpick [card = 1\<midarrow>2, expect = none]
   8.176 +nitpick [card = 1\<emdash>2, expect = none]
   8.177  apply simp
   8.178  done
   8.179  
   8.180  lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
   8.181 -nitpick [card = 1\<midarrow>2, expect = none]
   8.182 +nitpick [card = 1\<emdash>2, expect = none]
   8.183  apply simp
   8.184  done
   8.185  
   8.186 @@ -1153,17 +1153,17 @@
   8.187  oops
   8.188  
   8.189  lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
   8.190 -nitpick [card = 1\<midarrow>4, expect = none]
   8.191 +nitpick [card = 1\<emdash>4, expect = none]
   8.192  apply simp
   8.193  done
   8.194  
   8.195  lemma "Trie_rec_2 tr nil cons [] = nil"
   8.196 -nitpick [card = 1\<midarrow>4, expect = none]
   8.197 +nitpick [card = 1\<emdash>4, expect = none]
   8.198  apply simp
   8.199  done
   8.200  
   8.201  lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"
   8.202 -nitpick [card = 1\<midarrow>4, expect = none]
   8.203 +nitpick [card = 1\<emdash>4, expect = none]
   8.204  apply simp
   8.205  done
   8.206  
   8.207 @@ -1190,12 +1190,12 @@
   8.208  oops
   8.209  
   8.210  lemma "InfTree_rec leaf node Leaf = leaf"
   8.211 -nitpick [card = 1\<midarrow>3, expect = none]
   8.212 +nitpick [card = 1\<emdash>3, expect = none]
   8.213  apply simp
   8.214  done
   8.215  
   8.216  lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
   8.217 -nitpick [card = 1\<midarrow>3, expect = none]
   8.218 +nitpick [card = 1\<emdash>3, expect = none]
   8.219  apply simp
   8.220  done
   8.221  
   8.222 @@ -1214,22 +1214,22 @@
   8.223  oops
   8.224  
   8.225  lemma "P (Lam (\<lambda>a. Var a))"
   8.226 -nitpick [card = 1\<midarrow>5, expect = none]
   8.227 +nitpick [card = 1\<emdash>5, expect = none]
   8.228  nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
   8.229  oops
   8.230  
   8.231  lemma "lambda_rec var app lam (Var x) = var x"
   8.232 -nitpick [card = 1\<midarrow>3, expect = none]
   8.233 +nitpick [card = 1\<emdash>3, expect = none]
   8.234  apply simp
   8.235  done
   8.236  
   8.237  lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
   8.238 -nitpick [card = 1\<midarrow>3, expect = none]
   8.239 +nitpick [card = 1\<emdash>3, expect = none]
   8.240  apply simp
   8.241  done
   8.242  
   8.243  lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
   8.244 -nitpick [card = 1\<midarrow>3, expect = none]
   8.245 +nitpick [card = 1\<emdash>3, expect = none]
   8.246  apply simp
   8.247  done
   8.248  
   8.249 @@ -1255,27 +1255,27 @@
   8.250  oops
   8.251  
   8.252  lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
   8.253 -nitpick [card = 1\<midarrow>3, expect = none]
   8.254 +nitpick [card = 1\<emdash>3, expect = none]
   8.255  apply simp
   8.256  done
   8.257  
   8.258  lemma "U_rec_2 e c d nil cons (C x) = c x"
   8.259 -nitpick [card = 1\<midarrow>3, expect = none]
   8.260 +nitpick [card = 1\<emdash>3, expect = none]
   8.261  apply simp
   8.262  done
   8.263  
   8.264  lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
   8.265 -nitpick [card = 1\<midarrow>3, expect = none]
   8.266 +nitpick [card = 1\<emdash>3, expect = none]
   8.267  apply simp
   8.268  done
   8.269  
   8.270  lemma "U_rec_3 e c d nil cons [] = nil"
   8.271 -nitpick [card = 1\<midarrow>3, expect = none]
   8.272 +nitpick [card = 1\<emdash>3, expect = none]
   8.273  apply simp
   8.274  done
   8.275  
   8.276  lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)"
   8.277 -nitpick [card = 1\<midarrow>3, expect = none]
   8.278 +nitpick [card = 1\<emdash>3, expect = none]
   8.279  apply simp
   8.280  done
   8.281  

     9.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue May 24 00:01:33 2011 +0200
     9.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue May 24 00:01:33 2011 +0200
     9.3 @@ -11,7 +11,7 @@
     9.4  imports Complex_Main
     9.5  begin
     9.6  
     9.7 -nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
     9.8 +nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1,
     9.9                  timeout = 240]
    9.10  
    9.11  typedef three = "{0\<Colon>nat, 1, 2}"
    9.12 @@ -68,7 +68,7 @@
    9.13  sorry
    9.14  
    9.15  lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
    9.16 -nitpick [card = 1\<midarrow>5, expect = genuine]
    9.17 +nitpick [card = 1\<emdash>5, expect = genuine]
    9.18  oops
    9.19  
    9.20  lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))"
    9.21 @@ -96,11 +96,11 @@
    9.22  oops
    9.23  
    9.24  lemma "Pair a b = Abs_prod (Pair_Rep a b)"
    9.25 -nitpick [card = 1\<midarrow>2, expect = none]
    9.26 +nitpick [card = 1\<emdash>2, expect = none]
    9.27  by (rule Pair_def)
    9.28  
    9.29  lemma "Pair a b = Abs_prod (Pair_Rep b a)"
    9.30 -nitpick [card = 1\<midarrow>2, expect = none]
    9.31 +nitpick [card = 1\<emdash>2, expect = none]
    9.32  nitpick [dont_box, expect = genuine]
    9.33  oops
    9.34  
    9.35 @@ -109,7 +109,7 @@
    9.36  by (simp add: Pair_def [THEN sym])
    9.37  
    9.38  lemma "fst (Abs_prod (Pair_Rep a b)) = b"
    9.39 -nitpick [card = 1\<midarrow>2, expect = none]
    9.40 +nitpick [card = 1\<emdash>2, expect = none]
    9.41  nitpick [dont_box, expect = genuine]
    9.42  oops
    9.43  
    9.44 @@ -163,7 +163,7 @@
    9.45  by (rule Zero_int_def_raw)
    9.46  
    9.47  lemma "Abs_list (Rep_list a) = a"
    9.48 -nitpick [card = 1\<midarrow>2, expect = none]
    9.49 +nitpick [card = 1\<emdash>2, expect = none]
    9.50  by (rule Rep_list_inverse)
    9.51  
    9.52  record point =

    10.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue May 24 00:01:33 2011 +0200
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue May 24 00:01:33 2011 +0200
    10.3 @@ -352,11 +352,12 @@
    10.4            pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @
    10.5            pretty_serial_commas "and" pretties @
    10.6            pstrs (" " ^
    10.7 -          (if none_true monos then
    10.8 -             "passed the monotonicity test"
    10.9 -           else
   10.10 -             (if length pretties = 1 then "is" else "are") ^ " considered monotonic") ^
   10.11 -          ". " ^ extra))
   10.12 +                 (if none_true monos then
   10.13 +                    "passed the monotonicity test"
   10.14 +                  else
   10.15 +                    (if length pretties = 1 then "is" else "are") ^
   10.16 +                    " considered monotonic") ^
   10.17 +                 ". " ^ extra))
   10.18        end
   10.19      fun is_type_fundamentally_monotonic T =
   10.20        (is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso

    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue May 24 00:01:33 2011 +0200
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue May 24 00:01:33 2011 +0200
    11.3 @@ -38,7 +38,7 @@
    11.4  type raw_param = string * string list
    11.5  
    11.6  val default_default_params =
    11.7 -  [("card", "1\<midarrow>10"),
    11.8 +  [("card", "1\<emdash>10"),
    11.9     ("iter", "0,1,2,4,8,12,16,20,24,28"),
   11.10     ("bits", "1,2,3,4,6,8,10,12,14,16"),
   11.11     ("bisim_depth", "9"),
   11.12 @@ -148,7 +148,7 @@
   11.13    Data.map o fold (AList.update (op =)) o normalize_raw_param
   11.14  val default_raw_params = Data.get
   11.15  
   11.16 -fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
   11.17 +fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<emdash>")
   11.18  
   11.19  fun stringify_raw_param_value [] = ""
   11.20    | stringify_raw_param_value [s] = s
   11.21 @@ -187,7 +187,7 @@
   11.22        let
   11.23          val (k1, k2) =
   11.24            (case space_explode "-" s of
   11.25 -             [s] => the_default (s, s) (first_field "\<midarrow>" s)
   11.26 +             [s] => the_default (s, s) (first_field "\<emdash>" s)
   11.27             | ["", s2] => ("-" ^ s2, "-" ^ s2)
   11.28             | [s1, s2] => (s1, s2)
   11.29             | _ => raise Option)

    12.1 --- a/src/HOL/Tools/Nitpick/nitrox.ML	Tue May 24 00:01:33 2011 +0200
    12.2 +++ b/src/HOL/Tools/Nitpick/nitrox.ML	Tue May 24 00:01:33 2011 +0200
    12.3 @@ -2,7 +2,7 @@
    12.4      Author:     Jasmin Blanchette, TU Muenchen
    12.5      Copyright   2010, 2011
    12.6  
    12.7 -Finite model generation for TPTP first-order formulas via Nitpick.
    12.8 +Finite model generation for TPTP first-order formulas (FOF and CNF) via Nitpick.
    12.9  *)
   12.10  
   12.11  signature NITROX =
   12.12 @@ -182,8 +182,7 @@
   12.13  *)
   12.14        val state = Proof.init @{context}
   12.15        val params =
   12.16 -        [("card iota", "1\<midarrow>100"),
   12.17 -         ("card", "1\<midarrow>8"),
   12.18 +        [("card", "1\<emdash>8"),
   12.19           ("box", "false"),
   12.20           ("sat_solver", "smart"),
   12.21           ("max_threads", "1"),