src/HOL/Library/Permutation.thy
 changeset 60502 aa58872267ee parent 60495 d7ff0a1df90a parent 60500 903bb1495239 child 60515 484559628038
```     1.1 --- a/src/HOL/Library/Permutation.thy	Wed Jun 17 17:33:22 2015 +0200
1.2 +++ b/src/HOL/Library/Permutation.thy	Wed Jun 17 17:54:09 2015 +0200
1.3 @@ -2,7 +2,7 @@
1.4      Author:     Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker
1.5  *)
1.6
1.7 -section {* Permutations *}
1.8 +section \<open>Permutations\<close>
1.9
1.10  theory Permutation
1.11  imports Multiset
1.12 @@ -19,13 +19,13 @@
1.13    by (induct l) auto
1.14
1.15
1.16 -subsection {* Some examples of rule induction on permutations *}
1.17 +subsection \<open>Some examples of rule induction on permutations\<close>
1.18
1.19  lemma xperm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []"
1.20    by (induct xs == "[] :: 'a list" ys pred: perm) simp_all
1.21
1.22
1.23 -text {* \medskip This more general theorem is easier to understand! *}
1.24 +text \<open>\medskip This more general theorem is easier to understand!\<close>
1.25
1.26  lemma perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys"
1.27    by (induct pred: perm) simp_all
1.28 @@ -37,9 +37,9 @@
1.29    by (induct pred: perm) auto
1.30
1.31
1.32 -subsection {* Ways of making new permutations *}
1.33 +subsection \<open>Ways of making new permutations\<close>
1.34
1.35 -text {* We can insert the head anywhere in the list. *}
1.36 +text \<open>We can insert the head anywhere in the list.\<close>
1.37
1.38  lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
1.39    by (induct xs) auto
1.40 @@ -66,7 +66,7 @@
1.41    by (blast intro!: perm_append_swap perm_append1)
1.42
1.43
1.44 -subsection {* Further results *}
1.45 +subsection \<open>Further results\<close>
1.46
1.47  lemma perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []"
1.48    by (blast intro: perm_empty_imp)
1.49 @@ -86,13 +86,13 @@
1.50    by (blast dest: perm_sym)
1.51
1.52
1.53 -subsection {* Removing elements *}
1.54 +subsection \<open>Removing elements\<close>
1.55
1.56  lemma perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys"
1.57    by (induct ys) auto
1.58
1.59
1.60 -text {* \medskip Congruence rule *}
1.61 +text \<open>\medskip Congruence rule\<close>
1.62
1.63  lemma perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys"
1.64    by (induct pred: perm) auto
1.65 @@ -116,7 +116,7 @@
1.66    apply (safe intro!: perm_append2)
1.67    apply (rule append_perm_imp_perm)
1.68    apply (rule perm_append_swap [THEN perm.trans])
1.69 -    -- {* the previous step helps this @{text blast} call succeed quickly *}
1.70 +    -- \<open>the previous step helps this @{text blast} call succeed quickly\<close>
1.71    apply (blast intro: perm_append_swap)
1.72    done
1.73
1.74 @@ -241,7 +241,7 @@
1.75      assume "i < length xs"
1.76      with bij have "f i < length ys"
1.77        unfolding bij_betw_def by force
1.78 -    with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
1.79 +    with \<open>i < length xs\<close> show "xs ! i = zs ! (g \<circ> f) i"
1.80        using trans(1,3)[THEN perm_length] perm by auto
1.81    qed
1.82  qed
```