summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Set_Algebras.thy

changeset 60500 | 903bb1495239 |

parent 58881 | b9556a055632 |

child 60679 | ade12ef2773c |

1.1 --- a/src/HOL/Library/Set_Algebras.thy Wed Jun 17 10:57:11 2015 +0200 1.2 +++ b/src/HOL/Library/Set_Algebras.thy Wed Jun 17 11:03:05 2015 +0200 1.3 @@ -2,17 +2,17 @@ 1.4 Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM 1.5 *) 1.6 1.7 -section {* Algebraic operations on sets *} 1.8 +section \<open>Algebraic operations on sets\<close> 1.9 1.10 theory Set_Algebras 1.11 imports Main 1.12 begin 1.13 1.14 -text {* 1.15 +text \<open> 1.16 This library lifts operations like addition and multiplication to 1.17 sets. It was designed to support asymptotic calculations. See the 1.18 comments at the top of theory @{text BigO}. 1.19 -*} 1.20 +\<close> 1.21 1.22 instantiation set :: (plus) plus 1.23 begin 1.24 @@ -364,7 +364,7 @@ 1.25 then show ?case by (auto intro!: f) 1.26 next 1.27 case (insert x F) 1.28 - from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum S F)" 1.29 + from \<open>finite F\<close> \<open>\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)\<close> have "P (setsum S F)" 1.30 by induct auto 1.31 with insert show ?case 1.32 by (simp, subst f) auto