prefer plain ASCII / latex over not-so-universal Unicode;
authorwenzelm
Tue Apr 29 16:02:02 2014 +0200 (2014-04-29)
changeset 56790f54097170704
parent 56789 f377ddf1cc52
child 56791 23883e1879c5
prefer plain ASCII / latex over not-so-universal Unicode;
src/HOL/Library/Code_Abstract_Nat.thy
src/HOL/Library/RBT_Set.thy
src/HOL/List.thy
src/HOL/Relation.thy
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Tue Apr 29 16:00:34 2014 +0200
     1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Tue Apr 29 16:02:02 2014 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    The term @{term "Suc n"} is no longer a valid pattern.  Therefore,
     1.5    all occurrences of this term in a position where a pattern is
     1.6    expected (i.e.~on the left-hand side of a code equation) must be
     1.7 -  eliminated.  This can be accomplished – as far as possible – by
     1.8 +  eliminated.  This can be accomplished -- as far as possible -- by
     1.9    applying the following transformation rule:
    1.10  *}
    1.11  
     2.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Apr 29 16:00:34 2014 +0200
     2.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Apr 29 16:02:02 2014 +0200
     2.3 @@ -645,7 +645,7 @@
     2.4      by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
     2.5  qed
     2.6  
     2.7 -text {* A frequent case – avoid intermediate sets *}
     2.8 +text {* A frequent case -- avoid intermediate sets *}
     2.9  lemma [code_unfold]:
    2.10    "Set t1 \<subseteq> Set t2 \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
    2.11  by (simp add: subset_code Ball_Set)
     3.1 --- a/src/HOL/List.thy	Tue Apr 29 16:00:34 2014 +0200
     3.2 +++ b/src/HOL/List.thy	Tue Apr 29 16:02:02 2014 +0200
     3.3 @@ -6541,7 +6541,7 @@
     3.4    "List.coset [] \<le> set [] \<longleftrightarrow> False"
     3.5    by auto
     3.6  
     3.7 -text {* A frequent case – avoid intermediate sets *}
     3.8 +text {* A frequent case -- avoid intermediate sets *}
     3.9  lemma [code_unfold]:
    3.10    "set xs \<subseteq> set ys \<longleftrightarrow> list_all (\<lambda>x. x \<in> set ys) xs"
    3.11    by (auto simp: list_all_iff)
     4.1 --- a/src/HOL/Relation.thy	Tue Apr 29 16:00:34 2014 +0200
     4.2 +++ b/src/HOL/Relation.thy	Tue Apr 29 16:02:02 2014 +0200
     4.3 @@ -2,7 +2,7 @@
     4.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
     4.5  *)
     4.6  
     4.7 -header {* Relations – as sets of pairs, and binary predicates *}
     4.8 +header {* Relations -- as sets of pairs, and binary predicates *}
     4.9  
    4.10  theory Relation
    4.11  imports Finite_Set
     5.1 --- a/src/HOL/ex/Unification.thy	Tue Apr 29 16:00:34 2014 +0200
     5.2 +++ b/src/HOL/ex/Unification.thy	Tue Apr 29 16:02:02 2014 +0200
     5.3 @@ -24,7 +24,7 @@
     5.4    Ph.D. thesis, TUM, 1999, Sect. 5.8
     5.5  
     5.6    A Krauss, Partial and Nested Recursive Function Definitions in
     5.7 -  Higher-Order Logic, JAR 44(4):303–336, 2010. Sect. 6.3
     5.8 +  Higher-Order Logic, JAR 44(4):303-336, 2010. Sect. 6.3
     5.9  *}
    5.10  
    5.11