src/HOL/Nitpick_Examples/Manual_Nits.thy

 nitpick [dont_specialize, show_consts, expect = genuine]
 oops
 
 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
 
 subsection {* 3.4. Skolemization *}

 nitpick [verbose, expect = genuine]
 oops
 
 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 *}
 
 datatype tm = Var nat | Lam tm | App tm tm

 "subst\<^isub>2 \<sigma> (Lam t) =
  Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
 "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 *}
 
 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"

 
 lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
 (* 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
 
 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
 (* 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
 
 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"

 (* nitpick *)
 proof (induct t)
   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
 
 section {* 4. Case Studies *}
 

 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
 
 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:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
 nitpick [expect = genuine]

 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
 
 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 *}
 
 datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"

     N x k t u)"
 
 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
 "insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
 "insort\<^isub>1 (N y k t u) x =

 "insort\<^isub>2 (N y k t u) x =
  (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
                        (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