# HG changeset patch # User wenzelm # Date 1291405138 -3600 # Node ID b8703f63bfb2bc19c83e9e45101d762d2cd25deb # Parent fa22ae64ed85c78ca28dfdd4c275179885a6fb5c recoded latin1 as utf8; use textcomp for some text symbols where it appears appropriate; diff -r fa22ae64ed85 -r b8703f63bfb2 doc-src/TutorialI/Overview/Slides/main.tex --- 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 diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Algebra/document/root.tex --- 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 diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Auth/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Bali/Trans.thy --- 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 ,\ + Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\ *) (* @@ -372,8 +372,8 @@ assumes eval: "G\s0 \t\\ (v,s1)" shows trans: "G\(t,s0) \* (\Lit v\,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\ G\(t,s0) \* (t',s1) \ the_vals t' = v diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Equiv_Relations.thy --- 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 \ A \ A ==> finite (A//r)" -- {* recall @{thm equiv_type} *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Finite_Set.thy --- 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) ==> diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IMP/HoareEx.thy --- 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. *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IMP/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Abschannel.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Action.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Correctness.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Env.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Impl.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Impl_finite.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Lemmas.thy --- 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 diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Packet.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Receiver.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Sender.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ABP/Spec.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/NTP/Abschannel.thy --- 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) *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/Storage/Action.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/Storage/Correctness.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/Storage/Impl.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/Storage/Spec.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ex/TrivEx.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/ex/TrivEx2.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/Asig.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/Automata.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/IOA.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/Pred.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/Seq.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy --- 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. *) diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy --- 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 diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/Simulations.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/TL.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/TLS.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/IOA/meta_theory/Traces.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/Tutorial/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/HOLCF/ex/Dagstuhl.thy --- 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 *) (* ------------------------------------------------------------------------ *) diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Library/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Multivariate_Analysis/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/NSA/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Nominal/Examples/CR_Takahashi.thy --- 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 diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Old_Number_Theory/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Probability/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Proofs/Lambda/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/ex/SVC_Oracle.thy --- 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 *) diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/ex/Tarski.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/ex/document/root.tex --- 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} diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/ex/set.thy --- 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) \ f a = g b \ a \ X \ b \ X" by blast diff -r fa22ae64ed85 -r b8703f63bfb2 src/ZF/AC/WO6_WO1.thy --- 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. *) diff -r fa22ae64ed85 -r b8703f63bfb2 src/ZF/IMP/Com.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/ZF/IMP/Denotation.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/ZF/IMP/Equiv.thy --- 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 *} diff -r fa22ae64ed85 -r b8703f63bfb2 src/ZF/Induct/Brouwer.thy --- 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" diff -r fa22ae64ed85 -r b8703f63bfb2 src/ZF/Induct/document/root.tex --- 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}