Changes

Summary

revert accident with raw Unicode (not Isabelle symbols) in 7404f5b91e56;
changed precedence of big operators: now like any other function symbol
more canonical and less specialized syntax

Changeset 69747:2755c387f1e6 by wenzelm: revert accident with raw Unicode (not Isabelle symbols) in 7404f5b91e56;
The file was modified	`NEWS` (diff)
Changeset 69746:7404f5b91e56 by nipkow: changed precedence of big operators: now like any other function symbol
The file was modified	`NEWS` (diff)
Changeset 69745:aec42cee2521 by nipkow: more canonical and less specialized syntax
The file was modified	`src/HOL/Analysis/Abstract_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Arcwise_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Borel_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Caratheodory.thy` (diff)
The file was modified	`src/HOL/Analysis/Conformal_Mappings.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Normed_Spaces.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Function_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Further_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Analysis/Radon_Nikodym.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Analysis/Tagged_Division.thy` (diff)
The file was modified	`src/HOL/BNF_Composition.thy` (diff)
The file was modified	`src/HOL/Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Library/Disjoint_Sets.thy` (diff)
The file was modified	`src/HOL/Main.thy` (diff)
The file was modified	`src/HOL/Partial_Function.thy` (diff)
The file was modified	`src/HOL/UNITY/Transformers.thy` (diff)
The file was modified	`src/HOL/ex/Adhoc_Overloading_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Perm_Fragments.thy` (diff)