summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 29 Apr 2014 16:02:02 +0200 | |

changeset 56790 | f54097170704 |

parent 56789 | f377ddf1cc52 |

child 56791 | 23883e1879c5 |

prefer plain ASCII / latex over not-so-universal Unicode;

--- 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 *}