recoded latin1 as utf8;
use textcomp for some text symbols where it appears appropriate;

--- a/doc-src/TutorialI/Overview/Slides/main.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/doc-src/TutorialI/Overview/Slides/main.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -4,7 +4,7 @@
 \documentclass[pdf,nototal,myframes,slideColor,colorBG]{prosper}
 
 \usepackage{pstricks,pst-node,pst-text,pst-3d}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage{amsmath}
 
 
@@ -21,7 +21,7 @@
 \author{Tobias Nipkow
 \\{\small joint work with Larry Paulson and Markus Wenzel}
 }
-\institution{Technische Universität München
+\institution{Technische Universität München
 \\ \vspace{0.5cm}\includegraphics[scale=.4]{isabelle_hol}
 }
 \maketitle

--- a/src/HOL/Algebra/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Algebra/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -2,7 +2,8 @@
 \usepackage{graphicx}
 \usepackage{isabelle,isabellesym}
 \usepackage{amssymb}
-\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
+\usepackage[utf8]{inputenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 %\usepackage{amsmath}
 
@@ -17,8 +18,8 @@
 
 \title{The Isabelle/HOL Algebra Library}
 \author{Clemens Ballarin (Editor)}
-\date{With contributions by Jesús Aransay, Clemens Ballarin, Stephan Hohe,
-  Florian Kammüller and Lawrence C Paulson \\
+\date{With contributions by Jesús Aransay, Clemens Ballarin, Stephan Hohe,
+  Florian Kammüller and Lawrence C Paulson \\
   \today}
 \maketitle
 

--- a/src/HOL/Auth/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Auth/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -1,7 +1,7 @@
 \documentclass[10pt,a4paper,twoside]{article}
 \usepackage{graphicx}
 \usepackage{amssymb}
-\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}\urlstyle{rm}

--- a/src/HOL/Bali/Trans.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Bali/Trans.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -364,7 +364,7 @@
          
 (* Equivalenzen:
   Bigstep zu Smallstep komplett.
-  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
+  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
 *)
 
 (*
@@ -372,8 +372,8 @@
   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
     shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
 *)
-(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
-   Sowas blödes:
+(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
+   Sowas blödes:
    Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
    the_vals definieren\<dots>
   G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v

--- a/src/HOL/Equiv_Relations.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Equiv_Relations.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -315,7 +315,7 @@
 
 subsection {* Quotients and finiteness *}
 
-text {*Suggested by Florian Kammüller*}
+text {*Suggested by Florian Kammüller*}
 
 lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
   -- {* recall @{thm equiv_type} *}

--- a/src/HOL/Finite_Set.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -2277,7 +2277,7 @@
 apply (blast elim!: equalityE)
 done
 
-text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
+text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
 
 lemma dvd_partition:
   "finite (Union C) ==>

--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -8,7 +8,7 @@
 theory HoareEx imports Denotational begin
 
 text {*
-  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
+  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
   \cite{MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
   the correctness of the Hoare rule for while-loops.
 *}

--- a/src/HOL/HOLCF/IMP/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IMP/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -1,7 +1,7 @@
-
 \documentclass[11pt,a4paper]{article}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage{isabelle,isabellesym}
+\usepackage{textcomp}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Abschannel.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The transmission channel *}

--- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Abschannels.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The transmission channel -- finite version *}

--- a/src/HOL/HOLCF/IOA/ABP/Action.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Action.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Action.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The set of all actions of the system *}

--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Correctness.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The main correctness proof: System_fin implements System *}

--- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Impl.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The environment *}

--- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Impl.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The implementation *}

--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Impl.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The implementation *}

--- a/src/HOL/HOLCF/IOA/ABP/Lemmas.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Lemmas.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Lemmas.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 theory Lemmas

--- a/src/HOL/HOLCF/IOA/ABP/Packet.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Packet.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Packets *}

--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Receiver.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The implementation: receiver *}

--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Sender.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The implementation: sender *}

--- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Spec.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The specification of reliable transmission *}

--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/IOA/NTP/Abschannel.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The (faulty) transmission channel (both directions) *}

--- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/ABP/Action.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The set of all actions of the system *}

--- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/IOA/example/Correctness.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Correctness Proof *}

--- a/src/HOL/HOLCF/IOA/Storage/Impl.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/IOA/example/Spec.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The implementation of a memory *}

--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/IOA/example/Spec.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The specification of a memory *}

--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/TrivEx.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Trivial Abstraction Example *}

--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/TrivEx.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Trivial Abstraction Example with fairness *}

--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Abstraction Theory -- tailored for I/O automata *}

--- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/IOA/meta_theory/Asig.thy
-    Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
+    Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
 *)
 
 header {* Action signatures *}

--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Automata.thy
-    Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
+    Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
 *)
 
 header {* The I/O automata of Lynch and Tuttle in HOLCF *}

--- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/CompoExecs.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Compositionality on Execution level *}

--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Compositionality on Schedule level *}

--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *) 
 
 header {* Compositionality on Trace level *}

--- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Compositionality.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Compositionality of I/O automata *}

--- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Deadlock.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Deadlock freedom of I/O Automata *}

--- a/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/IOA.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* The theory of I/O automata in HOLCF *}

--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Live I/O automata -- specified by temproal formulas *}

--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Pred.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Logical Connectives lifted to predicates *}

--- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Correctness of Refinement Mappings in HOLCF/IOA *}

--- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Refinement Mappings in HOLCF/IOA *}

--- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Seq.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}

--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 
 Sequences over flat domains with lifted elements.
 *)

--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 theory ShortExecutions

--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/SimCorrectness.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Correctness of Simulations in HOLCF/IOA *}

--- a/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Simulations in HOLCF/IOA *}

--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* A General Temporal Logic *}

--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Temporal Logic of Steps -- tailored for I/O automata *}

--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Traces.thy
-    Author:     Olaf Müller
+    Author:     Olaf Müller
 *)
 
 header {* Executions and Traces of I/O automata in HOLCF *}

--- a/src/HOL/HOLCF/Tutorial/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/Tutorial/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -4,7 +4,7 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym}
 \usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

--- a/src/HOL/HOLCF/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -4,7 +4,7 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym}
 \usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

--- a/src/HOL/HOLCF/ex/Dagstuhl.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/HOLCF/ex/Dagstuhl.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -63,7 +63,7 @@
   done
 
 (* ------------------------------------------------------------------------ *)
-(* Zweite L"osung: Bernhard Möller                                          *)
+(* Zweite L"osung: Bernhard Möller                                          *)
 (* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
 (* verwendet lemma5                                                         *)
 (* ------------------------------------------------------------------------ *)

--- a/src/HOL/Library/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Library/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -1,8 +1,8 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{ifthen}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage[english]{babel}
-\usepackage{isabelle,isabellesym,amssymb,stmaryrd}
+\usepackage{isabelle,isabellesym,amssymb,stmaryrd,textcomp}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

--- a/src/HOL/Multivariate_Analysis/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -2,9 +2,8 @@
 % HOL/Multivariate_Analysis/document/root.tex
 
 \documentclass[11pt,a4paper]{article}
-\usepackage{graphicx,isabelle,isabellesym,latexsym}
+\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
 \usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[latin1]{inputenc}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

--- a/src/HOL/NSA/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/NSA/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -1,9 +1,5 @@
-
-% $Id$
-
 \documentclass[11pt,a4paper]{article}
-\usepackage{graphicx,isabelle,isabellesym,latexsym}
-\usepackage[latin1]{inputenc}
+\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -4,7 +4,7 @@
 (* This formalisation follows with some very slight exceptions    *)
 (* the version of this proof given by Randy Pollack in the paper: *)
 (*                                                                *)
-(*  Polishing Up the Tait-Martin Löf Proof of the                 *)
+(*  Polishing Up the Tait-Martin Löf Proof of the                 *)
 (*  Church-Rosser Theorem (1995).                                 *)
 
 theory CR_Takahashi

--- a/src/HOL/Old_Number_Theory/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Old_Number_Theory/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -1,8 +1,7 @@
-
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx}
 \usepackage{isabelle,isabellesym,pdfsetup}
-\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
 
 \urlstyle{rm}
 \isabellestyle{it}

--- a/src/HOL/Probability/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Probability/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -2,9 +2,9 @@
 % HOL/Multivariate_Analysis/document/root.tex
 
 \documentclass[11pt,a4paper]{article}
-\usepackage{graphicx,isabelle,isabellesym,latexsym}
+\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
 \usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

--- a/src/HOL/Proofs/Lambda/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Proofs/Lambda/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -1,8 +1,8 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx}
 \usepackage[english]{babel}
-\usepackage[latin1]{inputenc}
 \usepackage{amssymb}
+\usepackage{textcomp}
 \usepackage{isabelle,isabellesym,pdfsetup}
 
 \isabellestyle{it}

--- a/src/HOL/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -2,9 +2,10 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym}
 \usepackage{amssymb}
+\usepackage{textcomp}
 \usepackage[english]{babel}
 \usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

--- a/src/HOL/ex/SVC_Oracle.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson
     Copyright   1999  University of Cambridge
 
-Based upon the work of Søren T. Heilmann.
+Based upon the work of Søren T. Heilmann.
 *)
 
 header {* Installing an oracle for SVC (Stanford Validity Checker) *}
@@ -28,7 +28,7 @@
 The following code merely CALLS the oracle;
   the soundness-critical functions are at svc_funcs.ML
 
-Based upon the work of Søren T. Heilmann
+Based upon the work of Søren T. Heilmann
 *)
 
 

--- a/src/HOL/ex/Tarski.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/ex/Tarski.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/ex/Tarski.thy
     ID:         $Id$
-    Author:     Florian Kammüller, Cambridge University Computer Laboratory
+    Author:     Florian Kammüller, Cambridge University Computer Laboratory
 *)
 
 header {* The Full Theorem of Tarski *}

--- a/src/HOL/ex/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/ex/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -3,7 +3,7 @@
 
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage[english]{babel}
 \usepackage{textcomp}
 \usepackage{amssymb}

--- a/src/HOL/ex/set.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/ex/set.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -4,7 +4,7 @@
     Copyright   1991  University of Cambridge
 *)
 
-header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
+header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
 
 theory set imports Main begin
 
@@ -73,7 +73,7 @@
   by best
 
 
-subsection {* The Schröder-Berstein Theorem *}
+subsection {* The Schröder-Berstein Theorem *}
 
 lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
   by blast

--- a/src/ZF/AC/WO6_WO1.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/ZF/AC/WO6_WO1.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -6,7 +6,7 @@
 
 Every proof (except WO6 ==> WO1 and WO1 ==> WO2) are described as "clear"
 by Rubin & Rubin (page 2). 
-They refer reader to a book by Gödel to see the proof WO1 ==> WO2.
+They refer reader to a book by Gödel to see the proof WO1 ==> WO2.
 Fortunately order types made this proof also very easy.
 *)
 

--- a/src/ZF/IMP/Com.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/ZF/IMP/Com.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      ZF/IMP/Com.thy
-    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
+    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 *)
 
 header {* Arithmetic expressions, boolean expressions, commands *}

--- a/src/ZF/IMP/Denotation.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/ZF/IMP/Denotation.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      ZF/IMP/Denotation.thy
-    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
+    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 *)
 
 header {* Denotational semantics of expressions and commands *}

--- a/src/ZF/IMP/Equiv.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/ZF/IMP/Equiv.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -1,5 +1,5 @@
 (*  Title:      ZF/IMP/Equiv.thy
-    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
+    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 *)
 
 header {* Equivalence *}

--- a/src/ZF/Induct/Brouwer.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/ZF/Induct/Brouwer.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -39,7 +39,7 @@
   done
 
 
-subsection {* The Martin-Löf wellordering type *}
+subsection {* The Martin-Löf wellordering type *}
 
 consts
   Well :: "[i, i => i] => i"

--- a/src/ZF/Induct/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/ZF/Induct/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
@@ -1,7 +1,6 @@
-
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}