--- a/src/HOL/Library/Code_Abstract_Nat.thy Tue Apr 29 16:00:34 2014 +0200
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Tue Apr 29 16:02:02 2014 +0200
@@ -34,7 +34,7 @@
The term @{term "Suc n"} is no longer a valid pattern. Therefore,
all occurrences of this term in a position where a pattern is
expected (i.e.~on the left-hand side of a code equation) must be
- eliminated. This can be accomplished – as far as possible – by
+ eliminated. This can be accomplished -- as far as possible -- by
applying the following transformation rule:
*}
--- a/src/HOL/Library/RBT_Set.thy Tue Apr 29 16:00:34 2014 +0200
+++ b/src/HOL/Library/RBT_Set.thy Tue Apr 29 16:02:02 2014 +0200
@@ -645,7 +645,7 @@
by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
qed
-text {* A frequent case – avoid intermediate sets *}
+text {* A frequent case -- avoid intermediate sets *}
lemma [code_unfold]:
"Set t1 \<subseteq> Set t2 \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
by (simp add: subset_code Ball_Set)
--- a/src/HOL/List.thy Tue Apr 29 16:00:34 2014 +0200
+++ b/src/HOL/List.thy Tue Apr 29 16:02:02 2014 +0200
@@ -6541,7 +6541,7 @@
"List.coset [] \<le> set [] \<longleftrightarrow> False"
by auto
-text {* A frequent case – avoid intermediate sets *}
+text {* A frequent case -- avoid intermediate sets *}
lemma [code_unfold]:
"set xs \<subseteq> set ys \<longleftrightarrow> list_all (\<lambda>x. x \<in> set ys) xs"
by (auto simp: list_all_iff)
--- a/src/HOL/Relation.thy Tue Apr 29 16:00:34 2014 +0200
+++ b/src/HOL/Relation.thy Tue Apr 29 16:02:02 2014 +0200
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
*)
-header {* Relations – as sets of pairs, and binary predicates *}
+header {* Relations -- as sets of pairs, and binary predicates *}
theory Relation
imports Finite_Set
--- a/src/HOL/ex/Unification.thy Tue Apr 29 16:00:34 2014 +0200
+++ b/src/HOL/ex/Unification.thy Tue Apr 29 16:02:02 2014 +0200
@@ -24,7 +24,7 @@
Ph.D. thesis, TUM, 1999, Sect. 5.8
A Krauss, Partial and Nested Recursive Function Definitions in
- Higher-Order Logic, JAR 44(4):303–336, 2010. Sect. 6.3
+ Higher-Order Logic, JAR 44(4):303-336, 2010. Sect. 6.3
*}