recoded latin1 as utf8;
authorwenzelm
Fri Dec 03 20:38:58 2010 +0100 (2010-12-03)
changeset 40945b8703f63bfb2
parent 40944 fa22ae64ed85
child 40946 3f697c636fa1
recoded latin1 as utf8;
use textcomp for some text symbols where it appears appropriate;
doc-src/TutorialI/Overview/Slides/main.tex
src/HOL/Algebra/document/root.tex
src/HOL/Auth/document/root.tex
src/HOL/Bali/Trans.thy
src/HOL/Equiv_Relations.thy
src/HOL/Finite_Set.thy
src/HOL/HOLCF/IMP/HoareEx.thy
src/HOL/HOLCF/IMP/document/root.tex
src/HOL/HOLCF/IOA/ABP/Abschannel.thy
src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
src/HOL/HOLCF/IOA/ABP/Action.thy
src/HOL/HOLCF/IOA/ABP/Correctness.thy
src/HOL/HOLCF/IOA/ABP/Env.thy
src/HOL/HOLCF/IOA/ABP/Impl.thy
src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
src/HOL/HOLCF/IOA/ABP/Lemmas.thy
src/HOL/HOLCF/IOA/ABP/Packet.thy
src/HOL/HOLCF/IOA/ABP/Receiver.thy
src/HOL/HOLCF/IOA/ABP/Sender.thy
src/HOL/HOLCF/IOA/ABP/Spec.thy
src/HOL/HOLCF/IOA/NTP/Abschannel.thy
src/HOL/HOLCF/IOA/Storage/Action.thy
src/HOL/HOLCF/IOA/Storage/Correctness.thy
src/HOL/HOLCF/IOA/Storage/Impl.thy
src/HOL/HOLCF/IOA/Storage/Spec.thy
src/HOL/HOLCF/IOA/ex/TrivEx.thy
src/HOL/HOLCF/IOA/ex/TrivEx2.thy
src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOL/HOLCF/IOA/meta_theory/Asig.thy
src/HOL/HOLCF/IOA/meta_theory/Automata.thy
src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy
src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy
src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy
src/HOL/HOLCF/IOA/meta_theory/IOA.thy
src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOL/HOLCF/IOA/meta_theory/Pred.thy
src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOL/HOLCF/IOA/meta_theory/Seq.thy
src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOL/HOLCF/IOA/meta_theory/Simulations.thy
src/HOL/HOLCF/IOA/meta_theory/TL.thy
src/HOL/HOLCF/IOA/meta_theory/TLS.thy
src/HOL/HOLCF/IOA/meta_theory/Traces.thy
src/HOL/HOLCF/Tutorial/document/root.tex
src/HOL/HOLCF/document/root.tex
src/HOL/HOLCF/ex/Dagstuhl.thy
src/HOL/Library/document/root.tex
src/HOL/Multivariate_Analysis/document/root.tex
src/HOL/NSA/document/root.tex
src/HOL/Nominal/Examples/CR_Takahashi.thy
src/HOL/Old_Number_Theory/document/root.tex
src/HOL/Probability/document/root.tex
src/HOL/Proofs/Lambda/document/root.tex
src/HOL/document/root.tex
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/Tarski.thy
src/HOL/ex/document/root.tex
src/HOL/ex/set.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/IMP/Com.thy
src/ZF/IMP/Denotation.thy
src/ZF/IMP/Equiv.thy
src/ZF/Induct/Brouwer.thy
src/ZF/Induct/document/root.tex
     1.1 --- a/doc-src/TutorialI/Overview/Slides/main.tex	Fri Dec 03 20:26:57 2010 +0100
     1.2 +++ b/doc-src/TutorialI/Overview/Slides/main.tex	Fri Dec 03 20:38:58 2010 +0100
     1.3 @@ -4,7 +4,7 @@
     1.4  \documentclass[pdf,nototal,myframes,slideColor,colorBG]{prosper}
     1.5  
     1.6  \usepackage{pstricks,pst-node,pst-text,pst-3d}
     1.7 -\usepackage[latin1]{inputenc}
     1.8 +\usepackage[utf8]{inputenc}
     1.9  \usepackage{amsmath}
    1.10  
    1.11  
    1.12 @@ -21,7 +21,7 @@
    1.13  \author{Tobias Nipkow
    1.14  \\{\small joint work with Larry Paulson and Markus Wenzel}
    1.15  }
    1.16 -\institution{Technische Universität München
    1.17 +\institution{Technische Universität München
    1.18  \\ \vspace{0.5cm}\includegraphics[scale=.4]{isabelle_hol}
    1.19  }
    1.20  \maketitle
     2.1 --- a/src/HOL/Algebra/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
     2.2 +++ b/src/HOL/Algebra/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
     2.3 @@ -2,7 +2,8 @@
     2.4  \usepackage{graphicx}
     2.5  \usepackage{isabelle,isabellesym}
     2.6  \usepackage{amssymb}
     2.7 -\usepackage[latin1]{inputenc}
     2.8 +\usepackage{textcomp}
     2.9 +\usepackage[utf8]{inputenc}
    2.10  \usepackage[only,bigsqcap]{stmaryrd}
    2.11  %\usepackage{amsmath}
    2.12  
    2.13 @@ -17,8 +18,8 @@
    2.14  
    2.15  \title{The Isabelle/HOL Algebra Library}
    2.16  \author{Clemens Ballarin (Editor)}
    2.17 -\date{With contributions by Jesús Aransay, Clemens Ballarin, Stephan Hohe,
    2.18 -  Florian Kammüller and Lawrence C Paulson \\
    2.19 +\date{With contributions by Jesús Aransay, Clemens Ballarin, Stephan Hohe,
    2.20 +  Florian Kammüller and Lawrence C Paulson \\
    2.21    \today}
    2.22  \maketitle
    2.23  
     3.1 --- a/src/HOL/Auth/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
     3.2 +++ b/src/HOL/Auth/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  \documentclass[10pt,a4paper,twoside]{article}
     3.5  \usepackage{graphicx}
     3.6  \usepackage{amssymb}
     3.7 -\usepackage[latin1]{inputenc}
     3.8 +\usepackage{textcomp}
     3.9  \usepackage{latexsym,theorem}
    3.10  \usepackage{isabelle,isabellesym}
    3.11  \usepackage{pdfsetup}\urlstyle{rm}
     4.1 --- a/src/HOL/Bali/Trans.thy	Fri Dec 03 20:26:57 2010 +0100
     4.2 +++ b/src/HOL/Bali/Trans.thy	Fri Dec 03 20:38:58 2010 +0100
     4.3 @@ -364,7 +364,7 @@
     4.4           
     4.5  (* Equivalenzen:
     4.6    Bigstep zu Smallstep komplett.
     4.7 -  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
     4.8 +  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
     4.9  *)
    4.10  
    4.11  (*
    4.12 @@ -372,8 +372,8 @@
    4.13    assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
    4.14      shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
    4.15  *)
    4.16 -(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
    4.17 -   Sowas blödes:
    4.18 +(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
    4.19 +   Sowas blödes:
    4.20     Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
    4.21     the_vals definieren\<dots>
    4.22    G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
     5.1 --- a/src/HOL/Equiv_Relations.thy	Fri Dec 03 20:26:57 2010 +0100
     5.2 +++ b/src/HOL/Equiv_Relations.thy	Fri Dec 03 20:38:58 2010 +0100
     5.3 @@ -315,7 +315,7 @@
     5.4  
     5.5  subsection {* Quotients and finiteness *}
     5.6  
     5.7 -text {*Suggested by Florian Kammüller*}
     5.8 +text {*Suggested by Florian Kammüller*}
     5.9  
    5.10  lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
    5.11    -- {* recall @{thm equiv_type} *}
     6.1 --- a/src/HOL/Finite_Set.thy	Fri Dec 03 20:26:57 2010 +0100
     6.2 +++ b/src/HOL/Finite_Set.thy	Fri Dec 03 20:38:58 2010 +0100
     6.3 @@ -2277,7 +2277,7 @@
     6.4  apply (blast elim!: equalityE)
     6.5  done
     6.6  
     6.7 -text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
     6.8 +text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
     6.9  
    6.10  lemma dvd_partition:
    6.11    "finite (Union C) ==>
     7.1 --- a/src/HOL/HOLCF/IMP/HoareEx.thy	Fri Dec 03 20:26:57 2010 +0100
     7.2 +++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Fri Dec 03 20:38:58 2010 +0100
     7.3 @@ -8,7 +8,7 @@
     7.4  theory HoareEx imports Denotational begin
     7.5  
     7.6  text {*
     7.7 -  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
     7.8 +  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
     7.9    \cite{MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
    7.10    the correctness of the Hoare rule for while-loops.
    7.11  *}
     8.1 --- a/src/HOL/HOLCF/IMP/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
     8.2 +++ b/src/HOL/HOLCF/IMP/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
     8.3 @@ -1,7 +1,7 @@
     8.4 -
     8.5  \documentclass[11pt,a4paper]{article}
     8.6 -\usepackage[latin1]{inputenc}
     8.7 +\usepackage[utf8]{inputenc}
     8.8  \usepackage{isabelle,isabellesym}
     8.9 +\usepackage{textcomp}
    8.10  \usepackage{pdfsetup}
    8.11  
    8.12  \urlstyle{rm}
     9.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Fri Dec 03 20:26:57 2010 +0100
     9.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Fri Dec 03 20:38:58 2010 +0100
     9.3 @@ -1,5 +1,5 @@
     9.4  (*  Title:      HOLCF/IOA/ABP/Abschannel.thy
     9.5 -    Author:     Olaf Müller
     9.6 +    Author:     Olaf Müller
     9.7  *)
     9.8  
     9.9  header {* The transmission channel *}
    10.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Dec 03 20:26:57 2010 +0100
    10.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Dec 03 20:38:58 2010 +0100
    10.3 @@ -1,5 +1,5 @@
    10.4  (*  Title:      HOLCF/IOA/ABP/Abschannels.thy
    10.5 -    Author:     Olaf Müller
    10.6 +    Author:     Olaf Müller
    10.7  *)
    10.8  
    10.9  header {* The transmission channel -- finite version *}
    11.1 --- a/src/HOL/HOLCF/IOA/ABP/Action.thy	Fri Dec 03 20:26:57 2010 +0100
    11.2 +++ b/src/HOL/HOLCF/IOA/ABP/Action.thy	Fri Dec 03 20:38:58 2010 +0100
    11.3 @@ -1,5 +1,5 @@
    11.4  (*  Title:      HOLCF/IOA/ABP/Action.thy
    11.5 -    Author:     Olaf Müller
    11.6 +    Author:     Olaf Müller
    11.7  *)
    11.8  
    11.9  header {* The set of all actions of the system *}
    12.1 --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri Dec 03 20:26:57 2010 +0100
    12.2 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri Dec 03 20:38:58 2010 +0100
    12.3 @@ -1,5 +1,5 @@
    12.4  (*  Title:      HOLCF/IOA/ABP/Correctness.thy
    12.5 -    Author:     Olaf Müller
    12.6 +    Author:     Olaf Müller
    12.7  *)
    12.8  
    12.9  header {* The main correctness proof: System_fin implements System *}
    13.1 --- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Fri Dec 03 20:26:57 2010 +0100
    13.2 +++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Fri Dec 03 20:38:58 2010 +0100
    13.3 @@ -1,5 +1,5 @@
    13.4  (*  Title:      HOLCF/IOA/ABP/Impl.thy
    13.5 -    Author:     Olaf Müller
    13.6 +    Author:     Olaf Müller
    13.7  *)
    13.8  
    13.9  header {* The environment *}
    14.1 --- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Fri Dec 03 20:26:57 2010 +0100
    14.2 +++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Fri Dec 03 20:38:58 2010 +0100
    14.3 @@ -1,5 +1,5 @@
    14.4  (*  Title:      HOLCF/IOA/ABP/Impl.thy
    14.5 -    Author:     Olaf Müller
    14.6 +    Author:     Olaf Müller
    14.7  *)
    14.8  
    14.9  header {* The implementation *}
    15.1 --- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Fri Dec 03 20:26:57 2010 +0100
    15.2 +++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Fri Dec 03 20:38:58 2010 +0100
    15.3 @@ -1,5 +1,5 @@
    15.4  (*  Title:      HOLCF/IOA/ABP/Impl.thy
    15.5 -    Author:     Olaf Müller
    15.6 +    Author:     Olaf Müller
    15.7  *)
    15.8  
    15.9  header {* The implementation *}
    16.1 --- a/src/HOL/HOLCF/IOA/ABP/Lemmas.thy	Fri Dec 03 20:26:57 2010 +0100
    16.2 +++ b/src/HOL/HOLCF/IOA/ABP/Lemmas.thy	Fri Dec 03 20:38:58 2010 +0100
    16.3 @@ -1,5 +1,5 @@
    16.4  (*  Title:      HOLCF/IOA/ABP/Lemmas.thy
    16.5 -    Author:     Olaf Müller
    16.6 +    Author:     Olaf Müller
    16.7  *)
    16.8  
    16.9  theory Lemmas
    17.1 --- a/src/HOL/HOLCF/IOA/ABP/Packet.thy	Fri Dec 03 20:26:57 2010 +0100
    17.2 +++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy	Fri Dec 03 20:38:58 2010 +0100
    17.3 @@ -1,5 +1,5 @@
    17.4  (*  Title:      HOLCF/IOA/ABP/Packet.thy
    17.5 -    Author:     Olaf Müller
    17.6 +    Author:     Olaf Müller
    17.7  *)
    17.8  
    17.9  header {* Packets *}
    18.1 --- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Fri Dec 03 20:26:57 2010 +0100
    18.2 +++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Fri Dec 03 20:38:58 2010 +0100
    18.3 @@ -1,5 +1,5 @@
    18.4  (*  Title:      HOLCF/IOA/ABP/Receiver.thy
    18.5 -    Author:     Olaf Müller
    18.6 +    Author:     Olaf Müller
    18.7  *)
    18.8  
    18.9  header {* The implementation: receiver *}
    19.1 --- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Fri Dec 03 20:26:57 2010 +0100
    19.2 +++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Fri Dec 03 20:38:58 2010 +0100
    19.3 @@ -1,5 +1,5 @@
    19.4  (*  Title:      HOLCF/IOA/ABP/Sender.thy
    19.5 -    Author:     Olaf Müller
    19.6 +    Author:     Olaf Müller
    19.7  *)
    19.8  
    19.9  header {* The implementation: sender *}
    20.1 --- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Fri Dec 03 20:26:57 2010 +0100
    20.2 +++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Fri Dec 03 20:38:58 2010 +0100
    20.3 @@ -1,5 +1,5 @@
    20.4  (*  Title:      HOLCF/IOA/ABP/Spec.thy
    20.5 -    Author:     Olaf Müller
    20.6 +    Author:     Olaf Müller
    20.7  *)
    20.8  
    20.9  header {* The specification of reliable transmission *}
    21.1 --- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Fri Dec 03 20:26:57 2010 +0100
    21.2 +++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Fri Dec 03 20:38:58 2010 +0100
    21.3 @@ -1,5 +1,5 @@
    21.4  (*  Title:      HOL/IOA/NTP/Abschannel.thy
    21.5 -    Author:     Olaf Müller
    21.6 +    Author:     Olaf Müller
    21.7  *)
    21.8  
    21.9  header {* The (faulty) transmission channel (both directions) *}
    22.1 --- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Fri Dec 03 20:26:57 2010 +0100
    22.2 +++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Fri Dec 03 20:38:58 2010 +0100
    22.3 @@ -1,5 +1,5 @@
    22.4  (*  Title:      HOLCF/IOA/ABP/Action.thy
    22.5 -    Author:     Olaf Müller
    22.6 +    Author:     Olaf Müller
    22.7  *)
    22.8  
    22.9  header {* The set of all actions of the system *}
    23.1 --- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Fri Dec 03 20:26:57 2010 +0100
    23.2 +++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Fri Dec 03 20:38:58 2010 +0100
    23.3 @@ -1,5 +1,5 @@
    23.4  (*  Title:      HOL/IOA/example/Correctness.thy
    23.5 -    Author:     Olaf Müller
    23.6 +    Author:     Olaf Müller
    23.7  *)
    23.8  
    23.9  header {* Correctness Proof *}
    24.1 --- a/src/HOL/HOLCF/IOA/Storage/Impl.thy	Fri Dec 03 20:26:57 2010 +0100
    24.2 +++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy	Fri Dec 03 20:38:58 2010 +0100
    24.3 @@ -1,5 +1,5 @@
    24.4  (*  Title:      HOL/IOA/example/Spec.thy
    24.5 -    Author:     Olaf Müller
    24.6 +    Author:     Olaf Müller
    24.7  *)
    24.8  
    24.9  header {* The implementation of a memory *}
    25.1 --- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Fri Dec 03 20:26:57 2010 +0100
    25.2 +++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Fri Dec 03 20:38:58 2010 +0100
    25.3 @@ -1,5 +1,5 @@
    25.4  (*  Title:      HOL/IOA/example/Spec.thy
    25.5 -    Author:     Olaf Müller
    25.6 +    Author:     Olaf Müller
    25.7  *)
    25.8  
    25.9  header {* The specification of a memory *}
    26.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Fri Dec 03 20:26:57 2010 +0100
    26.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Fri Dec 03 20:38:58 2010 +0100
    26.3 @@ -1,5 +1,5 @@
    26.4  (*  Title:      HOLCF/IOA/TrivEx.thy
    26.5 -    Author:     Olaf Müller
    26.6 +    Author:     Olaf Müller
    26.7  *)
    26.8  
    26.9  header {* Trivial Abstraction Example *}
    27.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Fri Dec 03 20:26:57 2010 +0100
    27.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Fri Dec 03 20:38:58 2010 +0100
    27.3 @@ -1,5 +1,5 @@
    27.4  (*  Title:      HOLCF/IOA/TrivEx.thy
    27.5 -    Author:     Olaf Müller
    27.6 +    Author:     Olaf Müller
    27.7  *)
    27.8  
    27.9  header {* Trivial Abstraction Example with fairness *}
    28.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Fri Dec 03 20:26:57 2010 +0100
    28.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Fri Dec 03 20:38:58 2010 +0100
    28.3 @@ -1,5 +1,5 @@
    28.4  (*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
    28.5 -    Author:     Olaf Müller
    28.6 +    Author:     Olaf Müller
    28.7  *)
    28.8  
    28.9  header {* Abstraction Theory -- tailored for I/O automata *}
    29.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Fri Dec 03 20:26:57 2010 +0100
    29.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Fri Dec 03 20:38:58 2010 +0100
    29.3 @@ -1,5 +1,5 @@
    29.4  (*  Title:      HOL/IOA/meta_theory/Asig.thy
    29.5 -    Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
    29.6 +    Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
    29.7  *)
    29.8  
    29.9  header {* Action signatures *}
    30.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Fri Dec 03 20:26:57 2010 +0100
    30.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Fri Dec 03 20:38:58 2010 +0100
    30.3 @@ -1,5 +1,5 @@
    30.4  (*  Title:      HOLCF/IOA/meta_theory/Automata.thy
    30.5 -    Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
    30.6 +    Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
    30.7  *)
    30.8  
    30.9  header {* The I/O automata of Lynch and Tuttle in HOLCF *}
    31.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Fri Dec 03 20:26:57 2010 +0100
    31.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Fri Dec 03 20:38:58 2010 +0100
    31.3 @@ -1,5 +1,5 @@
    31.4  (*  Title:      HOLCF/IOA/meta_theory/CompoExecs.thy
    31.5 -    Author:     Olaf Müller
    31.6 +    Author:     Olaf Müller
    31.7  *)
    31.8  
    31.9  header {* Compositionality on Execution level *}
    32.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Fri Dec 03 20:26:57 2010 +0100
    32.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Fri Dec 03 20:38:58 2010 +0100
    32.3 @@ -1,5 +1,5 @@
    32.4  (*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
    32.5 -    Author:     Olaf Müller
    32.6 +    Author:     Olaf Müller
    32.7  *)
    32.8  
    32.9  header {* Compositionality on Schedule level *}
    33.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Fri Dec 03 20:26:57 2010 +0100
    33.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Fri Dec 03 20:38:58 2010 +0100
    33.3 @@ -1,5 +1,5 @@
    33.4  (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
    33.5 -    Author:     Olaf Müller
    33.6 +    Author:     Olaf Müller
    33.7  *) 
    33.8  
    33.9  header {* Compositionality on Trace level *}
    34.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Fri Dec 03 20:26:57 2010 +0100
    34.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Fri Dec 03 20:38:58 2010 +0100
    34.3 @@ -1,5 +1,5 @@
    34.4  (*  Title:      HOLCF/IOA/meta_theory/Compositionality.thy
    34.5 -    Author:     Olaf Müller
    34.6 +    Author:     Olaf Müller
    34.7  *)
    34.8  
    34.9  header {* Compositionality of I/O automata *}
    35.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Fri Dec 03 20:26:57 2010 +0100
    35.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Fri Dec 03 20:38:58 2010 +0100
    35.3 @@ -1,5 +1,5 @@
    35.4  (*  Title:      HOLCF/IOA/meta_theory/Deadlock.thy
    35.5 -    Author:     Olaf Müller
    35.6 +    Author:     Olaf Müller
    35.7  *)
    35.8  
    35.9  header {* Deadlock freedom of I/O Automata *}
    36.1 --- a/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Fri Dec 03 20:26:57 2010 +0100
    36.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Fri Dec 03 20:38:58 2010 +0100
    36.3 @@ -1,5 +1,5 @@
    36.4  (*  Title:      HOLCF/IOA/meta_theory/IOA.thy
    36.5 -    Author:     Olaf Müller
    36.6 +    Author:     Olaf Müller
    36.7  *)
    36.8  
    36.9  header {* The theory of I/O automata in HOLCF *}
    37.1 --- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Fri Dec 03 20:26:57 2010 +0100
    37.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Fri Dec 03 20:38:58 2010 +0100
    37.3 @@ -1,5 +1,5 @@
    37.4  (*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
    37.5 -    Author:     Olaf Müller
    37.6 +    Author:     Olaf Müller
    37.7  *)
    37.8  
    37.9  header {* Live I/O automata -- specified by temproal formulas *}
    38.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Fri Dec 03 20:26:57 2010 +0100
    38.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Fri Dec 03 20:38:58 2010 +0100
    38.3 @@ -1,5 +1,5 @@
    38.4  (*  Title:      HOLCF/IOA/meta_theory/Pred.thy
    38.5 -    Author:     Olaf Müller
    38.6 +    Author:     Olaf Müller
    38.7  *)
    38.8  
    38.9  header {* Logical Connectives lifted to predicates *}
    39.1 --- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Fri Dec 03 20:26:57 2010 +0100
    39.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Fri Dec 03 20:38:58 2010 +0100
    39.3 @@ -1,5 +1,5 @@
    39.4  (*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
    39.5 -    Author:     Olaf Müller
    39.6 +    Author:     Olaf Müller
    39.7  *)
    39.8  
    39.9  header {* Correctness of Refinement Mappings in HOLCF/IOA *}
    40.1 --- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Fri Dec 03 20:26:57 2010 +0100
    40.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Fri Dec 03 20:38:58 2010 +0100
    40.3 @@ -1,5 +1,5 @@
    40.4  (*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
    40.5 -    Author:     Olaf Müller
    40.6 +    Author:     Olaf Müller
    40.7  *)
    40.8  
    40.9  header {* Refinement Mappings in HOLCF/IOA *}
    41.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Fri Dec 03 20:26:57 2010 +0100
    41.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Fri Dec 03 20:38:58 2010 +0100
    41.3 @@ -1,5 +1,5 @@
    41.4  (*  Title:      HOLCF/IOA/meta_theory/Seq.thy
    41.5 -    Author:     Olaf Müller
    41.6 +    Author:     Olaf Müller
    41.7  *)
    41.8  
    41.9  header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
    42.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Fri Dec 03 20:26:57 2010 +0100
    42.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Fri Dec 03 20:38:58 2010 +0100
    42.3 @@ -1,5 +1,5 @@
    42.4  (*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
    42.5 -    Author:     Olaf Müller
    42.6 +    Author:     Olaf Müller
    42.7  
    42.8  Sequences over flat domains with lifted elements.
    42.9  *)
    43.1 --- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Fri Dec 03 20:26:57 2010 +0100
    43.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Fri Dec 03 20:38:58 2010 +0100
    43.3 @@ -1,5 +1,5 @@
    43.4  (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
    43.5 -    Author:     Olaf Müller
    43.6 +    Author:     Olaf Müller
    43.7  *)
    43.8  
    43.9  theory ShortExecutions
    44.1 --- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Fri Dec 03 20:26:57 2010 +0100
    44.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Fri Dec 03 20:38:58 2010 +0100
    44.3 @@ -1,5 +1,5 @@
    44.4  (*  Title:      HOLCF/IOA/meta_theory/SimCorrectness.thy
    44.5 -    Author:     Olaf Müller
    44.6 +    Author:     Olaf Müller
    44.7  *)
    44.8  
    44.9  header {* Correctness of Simulations in HOLCF/IOA *}
    45.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Fri Dec 03 20:26:57 2010 +0100
    45.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Fri Dec 03 20:38:58 2010 +0100
    45.3 @@ -1,5 +1,5 @@
    45.4  (*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
    45.5 -    Author:     Olaf Müller
    45.6 +    Author:     Olaf Müller
    45.7  *)
    45.8  
    45.9  header {* Simulations in HOLCF/IOA *}
    46.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Fri Dec 03 20:26:57 2010 +0100
    46.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Fri Dec 03 20:38:58 2010 +0100
    46.3 @@ -1,5 +1,5 @@
    46.4  (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
    46.5 -    Author:     Olaf Müller
    46.6 +    Author:     Olaf Müller
    46.7  *)
    46.8  
    46.9  header {* A General Temporal Logic *}
    47.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Fri Dec 03 20:26:57 2010 +0100
    47.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Fri Dec 03 20:38:58 2010 +0100
    47.3 @@ -1,5 +1,5 @@
    47.4  (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
    47.5 -    Author:     Olaf Müller
    47.6 +    Author:     Olaf Müller
    47.7  *)
    47.8  
    47.9  header {* Temporal Logic of Steps -- tailored for I/O automata *}
    48.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Fri Dec 03 20:26:57 2010 +0100
    48.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Fri Dec 03 20:38:58 2010 +0100
    48.3 @@ -1,5 +1,5 @@
    48.4  (*  Title:      HOLCF/IOA/meta_theory/Traces.thy
    48.5 -    Author:     Olaf Müller
    48.6 +    Author:     Olaf Müller
    48.7  *)
    48.8  
    48.9  header {* Executions and Traces of I/O automata in HOLCF *}
    49.1 --- a/src/HOL/HOLCF/Tutorial/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    49.2 +++ b/src/HOL/HOLCF/Tutorial/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    49.3 @@ -4,7 +4,7 @@
    49.4  \documentclass[11pt,a4paper]{article}
    49.5  \usepackage{graphicx,isabelle,isabellesym,latexsym}
    49.6  \usepackage[only,bigsqcap]{stmaryrd}
    49.7 -\usepackage[latin1]{inputenc}
    49.8 +\usepackage{textcomp}
    49.9  \usepackage{pdfsetup}
   49.10  
   49.11  \urlstyle{rm}
    50.1 --- a/src/HOL/HOLCF/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    50.2 +++ b/src/HOL/HOLCF/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    50.3 @@ -4,7 +4,7 @@
    50.4  \documentclass[11pt,a4paper]{article}
    50.5  \usepackage{graphicx,isabelle,isabellesym,latexsym}
    50.6  \usepackage[only,bigsqcap]{stmaryrd}
    50.7 -\usepackage[latin1]{inputenc}
    50.8 +\usepackage{textcomp}
    50.9  \usepackage{pdfsetup}
   50.10  
   50.11  \urlstyle{rm}
    51.1 --- a/src/HOL/HOLCF/ex/Dagstuhl.thy	Fri Dec 03 20:26:57 2010 +0100
    51.2 +++ b/src/HOL/HOLCF/ex/Dagstuhl.thy	Fri Dec 03 20:38:58 2010 +0100
    51.3 @@ -63,7 +63,7 @@
    51.4    done
    51.5  
    51.6  (* ------------------------------------------------------------------------ *)
    51.7 -(* Zweite L"osung: Bernhard Möller                                          *)
    51.8 +(* Zweite L"osung: Bernhard Möller                                          *)
    51.9  (* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
   51.10  (* verwendet lemma5                                                         *)
   51.11  (* ------------------------------------------------------------------------ *)
    52.1 --- a/src/HOL/Library/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    52.2 +++ b/src/HOL/Library/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    52.3 @@ -1,8 +1,8 @@
    52.4  \documentclass[11pt,a4paper]{article}
    52.5  \usepackage{ifthen}
    52.6 -\usepackage[latin1]{inputenc}
    52.7 +\usepackage[utf8]{inputenc}
    52.8  \usepackage[english]{babel}
    52.9 -\usepackage{isabelle,isabellesym,amssymb,stmaryrd}
   52.10 +\usepackage{isabelle,isabellesym,amssymb,stmaryrd,textcomp}
   52.11  \usepackage{pdfsetup}
   52.12  
   52.13  \urlstyle{rm}
    53.1 --- a/src/HOL/Multivariate_Analysis/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    53.2 +++ b/src/HOL/Multivariate_Analysis/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    53.3 @@ -2,9 +2,8 @@
    53.4  % HOL/Multivariate_Analysis/document/root.tex
    53.5  
    53.6  \documentclass[11pt,a4paper]{article}
    53.7 -\usepackage{graphicx,isabelle,isabellesym,latexsym}
    53.8 +\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
    53.9  \usepackage[only,bigsqcap]{stmaryrd}
   53.10 -\usepackage[latin1]{inputenc}
   53.11  \usepackage{pdfsetup}
   53.12  
   53.13  \urlstyle{rm}
    54.1 --- a/src/HOL/NSA/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    54.2 +++ b/src/HOL/NSA/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    54.3 @@ -1,9 +1,5 @@
    54.4 -
    54.5 -% $Id$
    54.6 -
    54.7  \documentclass[11pt,a4paper]{article}
    54.8 -\usepackage{graphicx,isabelle,isabellesym,latexsym}
    54.9 -\usepackage[latin1]{inputenc}
   54.10 +\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
   54.11  \usepackage{pdfsetup}
   54.12  
   54.13  \urlstyle{rm}
    55.1 --- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Dec 03 20:26:57 2010 +0100
    55.2 +++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Dec 03 20:38:58 2010 +0100
    55.3 @@ -4,7 +4,7 @@
    55.4  (* This formalisation follows with some very slight exceptions    *)
    55.5  (* the version of this proof given by Randy Pollack in the paper: *)
    55.6  (*                                                                *)
    55.7 -(*  Polishing Up the Tait-Martin Löf Proof of the                 *)
    55.8 +(*  Polishing Up the Tait-Martin Löf Proof of the                 *)
    55.9  (*  Church-Rosser Theorem (1995).                                 *)
   55.10  
   55.11  theory CR_Takahashi
    56.1 --- a/src/HOL/Old_Number_Theory/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    56.2 +++ b/src/HOL/Old_Number_Theory/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    56.3 @@ -1,8 +1,7 @@
    56.4 -
    56.5  \documentclass[11pt,a4paper]{article}
    56.6  \usepackage{graphicx}
    56.7  \usepackage{isabelle,isabellesym,pdfsetup}
    56.8 -\usepackage[latin1]{inputenc}
    56.9 +\usepackage{textcomp}
   56.10  
   56.11  \urlstyle{rm}
   56.12  \isabellestyle{it}
    57.1 --- a/src/HOL/Probability/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    57.2 +++ b/src/HOL/Probability/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    57.3 @@ -2,9 +2,9 @@
    57.4  % HOL/Multivariate_Analysis/document/root.tex
    57.5  
    57.6  \documentclass[11pt,a4paper]{article}
    57.7 -\usepackage{graphicx,isabelle,isabellesym,latexsym}
    57.8 +\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
    57.9  \usepackage[only,bigsqcap]{stmaryrd}
   57.10 -\usepackage[latin1]{inputenc}
   57.11 +\usepackage[utf8]{inputenc}
   57.12  \usepackage{pdfsetup}
   57.13  
   57.14  \urlstyle{rm}
    58.1 --- a/src/HOL/Proofs/Lambda/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    58.2 +++ b/src/HOL/Proofs/Lambda/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    58.3 @@ -1,8 +1,8 @@
    58.4  \documentclass[11pt,a4paper]{article}
    58.5  \usepackage{graphicx}
    58.6  \usepackage[english]{babel}
    58.7 -\usepackage[latin1]{inputenc}
    58.8  \usepackage{amssymb}
    58.9 +\usepackage{textcomp}
   58.10  \usepackage{isabelle,isabellesym,pdfsetup}
   58.11  
   58.12  \isabellestyle{it}
    59.1 --- a/src/HOL/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    59.2 +++ b/src/HOL/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    59.3 @@ -2,9 +2,10 @@
    59.4  \documentclass[11pt,a4paper]{article}
    59.5  \usepackage{graphicx,isabelle,isabellesym,latexsym}
    59.6  \usepackage{amssymb}
    59.7 +\usepackage{textcomp}
    59.8  \usepackage[english]{babel}
    59.9  \usepackage[only,bigsqcap]{stmaryrd}
   59.10 -\usepackage[latin1]{inputenc}
   59.11 +\usepackage[utf8]{inputenc}
   59.12  \usepackage{pdfsetup}
   59.13  
   59.14  \urlstyle{rm}
    60.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Dec 03 20:26:57 2010 +0100
    60.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Dec 03 20:38:58 2010 +0100
    60.3 @@ -3,7 +3,7 @@
    60.4      Author:     Lawrence C Paulson
    60.5      Copyright   1999  University of Cambridge
    60.6  
    60.7 -Based upon the work of Søren T. Heilmann.
    60.8 +Based upon the work of Søren T. Heilmann.
    60.9  *)
   60.10  
   60.11  header {* Installing an oracle for SVC (Stanford Validity Checker) *}
   60.12 @@ -28,7 +28,7 @@
   60.13  The following code merely CALLS the oracle;
   60.14    the soundness-critical functions are at svc_funcs.ML
   60.15  
   60.16 -Based upon the work of Søren T. Heilmann
   60.17 +Based upon the work of Søren T. Heilmann
   60.18  *)
   60.19  
   60.20  
    61.1 --- a/src/HOL/ex/Tarski.thy	Fri Dec 03 20:26:57 2010 +0100
    61.2 +++ b/src/HOL/ex/Tarski.thy	Fri Dec 03 20:38:58 2010 +0100
    61.3 @@ -1,6 +1,6 @@
    61.4  (*  Title:      HOL/ex/Tarski.thy
    61.5      ID:         $Id$
    61.6 -    Author:     Florian Kammüller, Cambridge University Computer Laboratory
    61.7 +    Author:     Florian Kammüller, Cambridge University Computer Laboratory
    61.8  *)
    61.9  
   61.10  header {* The Full Theorem of Tarski *}
    62.1 --- a/src/HOL/ex/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    62.2 +++ b/src/HOL/ex/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    62.3 @@ -3,7 +3,7 @@
    62.4  
    62.5  \documentclass[11pt,a4paper]{article}
    62.6  \usepackage{isabelle,isabellesym}
    62.7 -\usepackage[latin1]{inputenc}
    62.8 +\usepackage[utf8]{inputenc}
    62.9  \usepackage[english]{babel}
   62.10  \usepackage{textcomp}
   62.11  \usepackage{amssymb}
    63.1 --- a/src/HOL/ex/set.thy	Fri Dec 03 20:26:57 2010 +0100
    63.2 +++ b/src/HOL/ex/set.thy	Fri Dec 03 20:38:58 2010 +0100
    63.3 @@ -4,7 +4,7 @@
    63.4      Copyright   1991  University of Cambridge
    63.5  *)
    63.6  
    63.7 -header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
    63.8 +header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
    63.9  
   63.10  theory set imports Main begin
   63.11  
   63.12 @@ -73,7 +73,7 @@
   63.13    by best
   63.14  
   63.15  
   63.16 -subsection {* The Schröder-Berstein Theorem *}
   63.17 +subsection {* The Schröder-Berstein Theorem *}
   63.18  
   63.19  lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
   63.20    by blast
    64.1 --- a/src/ZF/AC/WO6_WO1.thy	Fri Dec 03 20:26:57 2010 +0100
    64.2 +++ b/src/ZF/AC/WO6_WO1.thy	Fri Dec 03 20:38:58 2010 +0100
    64.3 @@ -6,7 +6,7 @@
    64.4  
    64.5  Every proof (except WO6 ==> WO1 and WO1 ==> WO2) are described as "clear"
    64.6  by Rubin & Rubin (page 2). 
    64.7 -They refer reader to a book by Gödel to see the proof WO1 ==> WO2.
    64.8 +They refer reader to a book by Gödel to see the proof WO1 ==> WO2.
    64.9  Fortunately order types made this proof also very easy.
   64.10  *)
   64.11  
    65.1 --- a/src/ZF/IMP/Com.thy	Fri Dec 03 20:26:57 2010 +0100
    65.2 +++ b/src/ZF/IMP/Com.thy	Fri Dec 03 20:38:58 2010 +0100
    65.3 @@ -1,5 +1,5 @@
    65.4  (*  Title:      ZF/IMP/Com.thy
    65.5 -    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    65.6 +    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    65.7  *)
    65.8  
    65.9  header {* Arithmetic expressions, boolean expressions, commands *}
    66.1 --- a/src/ZF/IMP/Denotation.thy	Fri Dec 03 20:26:57 2010 +0100
    66.2 +++ b/src/ZF/IMP/Denotation.thy	Fri Dec 03 20:38:58 2010 +0100
    66.3 @@ -1,5 +1,5 @@
    66.4  (*  Title:      ZF/IMP/Denotation.thy
    66.5 -    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    66.6 +    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    66.7  *)
    66.8  
    66.9  header {* Denotational semantics of expressions and commands *}
    67.1 --- a/src/ZF/IMP/Equiv.thy	Fri Dec 03 20:26:57 2010 +0100
    67.2 +++ b/src/ZF/IMP/Equiv.thy	Fri Dec 03 20:38:58 2010 +0100
    67.3 @@ -1,5 +1,5 @@
    67.4  (*  Title:      ZF/IMP/Equiv.thy
    67.5 -    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    67.6 +    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    67.7  *)
    67.8  
    67.9  header {* Equivalence *}
    68.1 --- a/src/ZF/Induct/Brouwer.thy	Fri Dec 03 20:26:57 2010 +0100
    68.2 +++ b/src/ZF/Induct/Brouwer.thy	Fri Dec 03 20:38:58 2010 +0100
    68.3 @@ -39,7 +39,7 @@
    68.4    done
    68.5  
    68.6  
    68.7 -subsection {* The Martin-Löf wellordering type *}
    68.8 +subsection {* The Martin-Löf wellordering type *}
    68.9  
   68.10  consts
   68.11    Well :: "[i, i => i] => i"
    69.1 --- a/src/ZF/Induct/document/root.tex	Fri Dec 03 20:26:57 2010 +0100
    69.2 +++ b/src/ZF/Induct/document/root.tex	Fri Dec 03 20:38:58 2010 +0100
    69.3 @@ -1,7 +1,6 @@
    69.4 -
    69.5  \documentclass[11pt,a4paper]{article}
    69.6  \usepackage{isabelle,isabellesym}
    69.7 -\usepackage[latin1]{inputenc}
    69.8 +\usepackage[utf8]{inputenc}
    69.9  \usepackage{pdfsetup}
   69.10  
   69.11  \urlstyle{rm}