# HG changeset patch
# User wenzelm
# Date 1398780122 -7200
# Node ID f5409717070495a11da3f688844ff138002124ae
# Parent  f377ddf1cc522adeb0569f56fc9b6dbb88a5e302
prefer plain ASCII / latex over not-so-universal Unicode;

diff -r f377ddf1cc52 -r f54097170704 src/HOL/Library/Code_Abstract_Nat.thy
--- 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:
 *}
 
diff -r f377ddf1cc52 -r f54097170704 src/HOL/Library/RBT_Set.thy
--- 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)
diff -r f377ddf1cc52 -r f54097170704 src/HOL/List.thy
--- 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)
diff -r f377ddf1cc52 -r f54097170704 src/HOL/Relation.thy
--- 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
diff -r f377ddf1cc52 -r f54097170704 src/HOL/ex/Unification.thy
--- 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
 *}