# HG changeset patch
# User blanchet
# Date 1306188093 -7200
# Node ID ee829022381dc5de1769ed3fd8b62bf3e0d594d7
# Parent  034fc4d0c9093c2631fefbf77f35ae274b24b324
use \<emdash> rather than \<midarrow>

diff -r 034fc4d0c909 -r ee829022381d doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue May 24 00:01:33 2011 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Tue May 24 00:01:33 2011 +0200
@@ -346,7 +346,7 @@
 \prew
 \textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
 can be entered as \texttt{-} (hyphen) or
-\texttt{\char`\\\char`\<midarrow\char`\>}.} \\[2\smallskipamount]
+\texttt{\char`\\\char`\<emdash\char`\>}.} \\[2\smallskipamount]
 \slshape Nitpick found no counterexample.
 \postw
 
@@ -1890,7 +1890,7 @@
 \item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
-of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
+of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<emdash\char`\>}.
 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
 \item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
 (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue May 24 00:01:33 2011 +0200
@@ -11,29 +11,29 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0,
+nitpick_params [verbose, card = 1\<emdash>6, unary_ints, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 subsection {* Curry in a Hurry *}
 
 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<emdash>12, expect = none]
 by auto
 
 lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<emdash>12, expect = none]
 by auto
 
 lemma "split (curry f) = f"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<emdash>12, expect = none]
 by auto
 
 lemma "curry (split f) = f"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<emdash>12, expect = none]
 by auto
 
 lemma "split (\<lambda>x y. f (x, y)) = f"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<emdash>12, expect = none]
 by auto
 
 subsection {* Representations *}
@@ -44,7 +44,7 @@
 
 lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
 nitpick [card 'a = 25, card 'b = 24, expect = genuine]
-nitpick [card = 1\<midarrow>10, mono, expect = none]
+nitpick [card = 1\<emdash>10, mono, expect = none]
 oops
 
 lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
@@ -56,39 +56,39 @@
 oops
 
 lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<emdash>12, expect = none]
 by auto
 
 lemma "fst (a, b) = a"
-nitpick [card = 1\<midarrow>20, expect = none]
+nitpick [card = 1\<emdash>20, expect = none]
 by auto
 
 lemma "\<exists>P. P = Id"
-nitpick [card = 1\<midarrow>20, expect = none]
+nitpick [card = 1\<emdash>20, expect = none]
 by auto
 
 lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 by auto
 
 lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 by auto
 
 lemma "Id (a, a)"
-nitpick [card = 1\<midarrow>50, expect = none]
+nitpick [card = 1\<emdash>50, expect = none]
 by (auto simp: Id_def Collect_def)
 
 lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
-nitpick [card = 1\<midarrow>10, expect = none]
+nitpick [card = 1\<emdash>10, expect = none]
 by (auto simp: Id_def Collect_def)
 
 lemma "UNIV (x\<Colon>'a\<times>'a)"
-nitpick [card = 1\<midarrow>50, expect = none]
+nitpick [card = 1\<emdash>50, expect = none]
 sorry
 
 lemma "{} = A - A"
-nitpick [card = 1\<midarrow>100, expect = none]
+nitpick [card = 1\<emdash>100, expect = none]
 by auto
 
 lemma "g = Let (A \<or> B)"
@@ -132,7 +132,7 @@
 oops
 
 lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
-nitpick [card = 1\<midarrow>10, expect = none]
+nitpick [card = 1\<emdash>10, expect = none]
 by auto
 
 lemma "\<exists>F. F a b = G a b"
@@ -149,7 +149,7 @@
 
 lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
        A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
-nitpick [card = 1\<midarrow>25, expect = none]
+nitpick [card = 1\<emdash>25, expect = none]
 by auto
 
 lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
@@ -174,19 +174,19 @@
 oops
 
 lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
-nitpick [card 'a = 1\<midarrow>15, expect = none]
+nitpick [card 'a = 1\<emdash>15, expect = none]
 by auto
 
 lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
-nitpick [card = 1\<midarrow>15, expect = none]
+nitpick [card = 1\<emdash>15, expect = none]
 by auto
 
 lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 by auto
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 by auto
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
@@ -195,42 +195,42 @@
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
        f u v w x y z = f u (g u) w (h u w) y (k u w y)"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 sorry
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
        f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
-nitpick [card = 1\<midarrow>2, expect = genuine]
+nitpick [card = 1\<emdash>2, expect = genuine]
 oops
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
        f u v w x y z = f u (g u w) w (h u w) y (k u w y)"
-nitpick [card = 1\<midarrow>2, expect = genuine]
+nitpick [card = 1\<emdash>2, expect = genuine]
 oops
 
 lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
        f u v w x = f u (g u) w (h u w)"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 sorry
 
 lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
        f u v w x = f u (g u w) w (h u)"
-nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
+nitpick [card = 1\<emdash>2, dont_box, expect = genuine]
 oops
 
 lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
        f u v w x = f u (g u) w (h u w)"
-nitpick [card = 1\<midarrow>2, dont_box, expect = none]
+nitpick [card = 1\<emdash>2, dont_box, expect = none]
 sorry
 
 lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
        f u v w x = f u (g u w) w (h u)"
-nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
+nitpick [card = 1\<emdash>2, dont_box, expect = genuine]
 oops
 
 lemma "\<forall>x. if (\<forall>y. x = y) then False else True"
 nitpick [card = 1, expect = genuine]
-nitpick [card = 2\<midarrow>5, expect = none]
+nitpick [card = 2\<emdash>5, expect = none]
 oops
 
 lemma "\<forall>x\<Colon>'a\<times>'b. if (\<forall>y. x = y) then False else True"
@@ -323,15 +323,15 @@
 oops
 
 lemma "P x \<equiv> P x"
-nitpick [card = 1\<midarrow>10, expect = none]
+nitpick [card = 1\<emdash>10, expect = none]
 by auto
 
 lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x"
-nitpick [card = 1\<midarrow>10, expect = none]
+nitpick [card = 1\<emdash>10, expect = none]
 by auto
 
 lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x"
-nitpick [card = 1\<midarrow>10, expect = none]
+nitpick [card = 1\<emdash>10, expect = none]
 by auto
 
 lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False"
@@ -343,7 +343,7 @@
 by auto
 
 lemma "P x \<Longrightarrow> P x"
-nitpick [card = 1\<midarrow>10, expect = none]
+nitpick [card = 1\<emdash>10, expect = none]
 by auto
 
 lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False"
@@ -604,11 +604,11 @@
 by simp
 
 lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 by auto
 
 lemma "rtrancl = (\<lambda>x. rtrancl x \<union> {(y, y)})"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply (rule ext)
 by auto
 
@@ -617,11 +617,11 @@
 by auto
 
 lemma "((x, x), (x, x)) \<in> rtrancl {}"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 by auto
 
 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 by auto
 
 lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
@@ -629,27 +629,27 @@
 by auto
 
 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 by auto
 
 lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 by auto
 
 lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 by auto
 
 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 by auto
 
 lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 by auto
 
 lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 by auto
 
 lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B"
@@ -661,7 +661,7 @@
 by auto
 
 lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"
-nitpick [card = 1\<midarrow>7, expect = none]
+nitpick [card = 1\<emdash>7, expect = none]
 by auto
 
 lemma "A \<union> - A = UNIV"
@@ -695,7 +695,7 @@
 oops
 
 lemma "\<exists>x. x = The"
-nitpick [card = 1\<midarrow>3]
+nitpick [card = 1\<emdash>3]
 by auto
 
 lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x"
@@ -708,11 +708,11 @@
 
 lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = x \<or> The P = y"
 nitpick [card = 2, expect = none]
-nitpick [card = 3\<midarrow>5, expect = genuine]
+nitpick [card = 3\<emdash>5, expect = genuine]
 oops
 
 lemma "P x \<Longrightarrow> P (The P)"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 nitpick [card = 8, expect = genuine]
 oops
 
@@ -721,7 +721,7 @@
 oops
 
 lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 by auto
 
 lemma "x = Eps"
@@ -729,7 +729,7 @@
 oops
 
 lemma "\<exists>x. x = Eps"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 by auto
 
 lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x"
@@ -742,7 +742,7 @@
 oops
 
 lemma "P x \<Longrightarrow> P (Eps P)"
-nitpick [card = 1\<midarrow>8, expect = none]
+nitpick [card = 1\<emdash>8, expect = none]
 by (metis exE_some)
 
 lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y"
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Tue May 24 00:01:33 2011 +0200
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<midarrow>8, max_potential = 0,
+nitpick_params [verbose, card = 1\<emdash>8, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 primrec rot where
@@ -23,7 +23,7 @@
 "rot NibbleF = Nibble0"
 
 lemma "rot n \<noteq> n"
-nitpick [card = 1\<midarrow>8,16, verbose, expect = none]
+nitpick [card = 1\<emdash>8,16, verbose, expect = none]
 sorry
 
 lemma "rot Nibble2 \<noteq> Nibble3"
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Induct_Nits.thy
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue May 24 00:01:33 2011 +0200
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<midarrow>8, unary_ints,
+nitpick_params [verbose, card = 1\<emdash>8, unary_ints,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 inductive p1 :: "nat \<Rightarrow> bool" where
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue May 24 00:01:33 2011 +0200
@@ -11,7 +11,7 @@
 imports Nitpick
 begin
 
-nitpick_params [verbose, card = 1\<midarrow>5, bits = 1,2,3,4,6,
+nitpick_params [verbose, card = 1\<emdash>5, bits = 1,2,3,4,6,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 lemma "Suc x = x + 1"
@@ -187,7 +187,7 @@
 
 lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)"
 nitpick [unary_ints, expect = none]
-nitpick [binary_ints, card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
+nitpick [binary_ints, card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
 sorry
 
 lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))"
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue May 24 00:01:33 2011 +0200
@@ -44,7 +44,7 @@
 
 lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
 nitpick [expect = none]
-nitpick [card 'a = 1\<midarrow>50, expect = none]
+nitpick [card 'a = 1\<emdash>50, expect = none]
 (* sledgehammer *)
 apply (metis the_equality)
 done
@@ -227,7 +227,7 @@
 
 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
 nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
 subsection {* 3.10. Boxing *}
@@ -263,7 +263,7 @@
 "subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
 
 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
 subsection {* 3.11. Scope Monotonicity *}
@@ -288,7 +288,7 @@
 (* nitpick *)
 apply (induct set: reach)
   apply auto
- nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
+ nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
  apply (thin_tac "n \<in> reach")
  nitpick [expect = genuine]
 oops
@@ -297,7 +297,7 @@
 (* nitpick *)
 apply (induct set: reach)
   apply auto
- nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
+ nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
  apply (thin_tac "n \<in> reach")
  nitpick [expect = genuine]
 oops
@@ -336,7 +336,7 @@
   case Leaf thus ?case by simp
 next
   case (Branch t u) thus ?case
-  nitpick [non_std, card = 1\<midarrow>4, expect = none]
+  nitpick [non_std, card = 1\<emdash>4, expect = none]
   by auto
 qed
 
@@ -384,7 +384,7 @@
 
 theorem S\<^isub>3_sound:
 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
 theorem S\<^isub>3_complete:
@@ -403,19 +403,19 @@
 
 theorem S\<^isub>4_sound:
 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
 theorem S\<^isub>4_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
 theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
 "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
 "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
 "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
 subsection {* 4.2. AA Trees *}
@@ -469,13 +469,13 @@
 theorem dataset_skew_split:
 "dataset (skew t) = dataset t"
 "dataset (split t) = dataset t"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
 theorem wf_skew_split:
 "wf t \<Longrightarrow> skew t = t"
 "wf t \<Longrightarrow> split t = t"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
 primrec insort\<^isub>1 where
@@ -499,11 +499,11 @@
                        (if x > y then insort\<^isub>2 u x else u))"
 
 theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
 theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
 end
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Record_Nits.thy
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Tue May 24 00:01:33 2011 +0200
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
+nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 record point2d =
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue May 24 00:01:33 2011 +0200
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
+nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 lemma "P \<and> Q"
@@ -283,7 +283,7 @@
 text {* ``Every point is a fixed point of some function.'' *}
 
 lemma "\<exists>f. f x = x"
-nitpick [card = 1\<midarrow>7, expect = none]
+nitpick [card = 1\<emdash>7, expect = none]
 apply (rule_tac x = "\<lambda>x. x" in exI)
 apply simp
 done
@@ -745,7 +745,7 @@
 oops
 
 lemma "T3_rec e (E x) = e x"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 apply simp
 done
 
@@ -774,7 +774,7 @@
 oops
 
 lemma "P Suc"
-nitpick [card = 1\<midarrow>7, expect = none]
+nitpick [card = 1\<emdash>7, expect = none]
 oops
 
 lemma "nat_rec zero suc 0 = zero"
@@ -810,12 +810,12 @@
 oops
 
 lemma "list_rec nil cons [] = nil"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 apply simp
 done
 
 lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 apply simp
 done
 
@@ -888,7 +888,7 @@
 done
 
 lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 apply simp
 done
 
@@ -926,12 +926,12 @@
 oops
 
 lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
 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)"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
@@ -944,7 +944,7 @@
 oops
 
 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)"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
@@ -1004,32 +1004,32 @@
 oops
 
 lemma "X_Y_rec_1 a b c d e f A = a"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 apply simp
 done
 
 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)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 apply simp
 done
 
 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)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 apply simp
 done
 
 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)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 apply simp
 done
 
 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)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 apply simp
 done
 
 lemma "X_Y_rec_2 a b c d e f F = f"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 apply simp
 done
 
@@ -1060,32 +1060,32 @@
 oops
 
 lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 apply simp
 done
 
 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))"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
 lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 apply simp
 done
 
 lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 apply simp
 done
 
 lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 apply simp
 done
 
 lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 apply simp
 done
 
@@ -1116,17 +1116,17 @@
 oops
 
 lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 apply simp
 done
 
 lemma "YOpt_rec_2 cy n s None = n"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 apply simp
 done
 
 lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 apply simp
 done
 
@@ -1153,17 +1153,17 @@
 oops
 
 lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 apply simp
 done
 
 lemma "Trie_rec_2 tr nil cons [] = nil"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 apply simp
 done
 
 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)"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<emdash>4, expect = none]
 apply simp
 done
 
@@ -1190,12 +1190,12 @@
 oops
 
 lemma "InfTree_rec leaf node Leaf = leaf"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
 lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
@@ -1214,22 +1214,22 @@
 oops
 
 lemma "P (Lam (\<lambda>a. Var a))"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<emdash>5, expect = none]
 nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
 oops
 
 lemma "lambda_rec var app lam (Var x) = var x"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
 lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
 lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
@@ -1255,27 +1255,27 @@
 oops
 
 lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
 lemma "U_rec_2 e c d nil cons (C x) = c x"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
 lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
 lemma "U_rec_3 e c d nil cons [] = nil"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
 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)"
-nitpick [card = 1\<midarrow>3, expect = none]
+nitpick [card = 1\<emdash>3, expect = none]
 apply simp
 done
 
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue May 24 00:01:33 2011 +0200
@@ -11,7 +11,7 @@
 imports Complex_Main
 begin
 
-nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
+nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1,
                 timeout = 240]
 
 typedef three = "{0\<Colon>nat, 1, 2}"
@@ -68,7 +68,7 @@
 sorry
 
 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
-nitpick [card = 1\<midarrow>5, expect = genuine]
+nitpick [card = 1\<emdash>5, expect = genuine]
 oops
 
 lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))"
@@ -96,11 +96,11 @@
 oops
 
 lemma "Pair a b = Abs_prod (Pair_Rep a b)"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 by (rule Pair_def)
 
 lemma "Pair a b = Abs_prod (Pair_Rep b a)"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 nitpick [dont_box, expect = genuine]
 oops
 
@@ -109,7 +109,7 @@
 by (simp add: Pair_def [THEN sym])
 
 lemma "fst (Abs_prod (Pair_Rep a b)) = b"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 nitpick [dont_box, expect = genuine]
 oops
 
@@ -163,7 +163,7 @@
 by (rule Zero_int_def_raw)
 
 lemma "Abs_list (Rep_list a) = a"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 by (rule Rep_list_inverse)
 
 record point =
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue May 24 00:01:33 2011 +0200
@@ -352,11 +352,12 @@
           pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @
           pretty_serial_commas "and" pretties @
           pstrs (" " ^
-          (if none_true monos then
-             "passed the monotonicity test"
-           else
-             (if length pretties = 1 then "is" else "are") ^ " considered monotonic") ^
-          ". " ^ extra))
+                 (if none_true monos then
+                    "passed the monotonicity test"
+                  else
+                    (if length pretties = 1 then "is" else "are") ^
+                    " considered monotonic") ^
+                 ". " ^ extra))
       end
     fun is_type_fundamentally_monotonic T =
       (is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue May 24 00:01:33 2011 +0200
@@ -38,7 +38,7 @@
 type raw_param = string * string list
 
 val default_default_params =
-  [("card", "1\<midarrow>10"),
+  [("card", "1\<emdash>10"),
    ("iter", "0,1,2,4,8,12,16,20,24,28"),
    ("bits", "1,2,3,4,6,8,10,12,14,16"),
    ("bisim_depth", "9"),
@@ -148,7 +148,7 @@
   Data.map o fold (AList.update (op =)) o normalize_raw_param
 val default_raw_params = Data.get
 
-fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
+fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<emdash>")
 
 fun stringify_raw_param_value [] = ""
   | stringify_raw_param_value [s] = s
@@ -187,7 +187,7 @@
       let
         val (k1, k2) =
           (case space_explode "-" s of
-             [s] => the_default (s, s) (first_field "\<midarrow>" s)
+             [s] => the_default (s, s) (first_field "\<emdash>" s)
            | ["", s2] => ("-" ^ s2, "-" ^ s2)
            | [s1, s2] => (s1, s2)
            | _ => raise Option)
diff -r 034fc4d0c909 -r ee829022381d src/HOL/Tools/Nitpick/nitrox.ML
--- a/src/HOL/Tools/Nitpick/nitrox.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML	Tue May 24 00:01:33 2011 +0200
@@ -2,7 +2,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2010, 2011
 
-Finite model generation for TPTP first-order formulas via Nitpick.
+Finite model generation for TPTP first-order formulas (FOF and CNF) via Nitpick.
 *)
 
 signature NITROX =
@@ -182,8 +182,7 @@
 *)
       val state = Proof.init @{context}
       val params =
-        [("card iota", "1\<midarrow>100"),
-         ("card", "1\<midarrow>8"),
+        [("card", "1\<emdash>8"),
          ("box", "false"),
          ("sat_solver", "smart"),
          ("max_threads", "1"),