# HG changeset patch
# User wenzelm
# Date 1291327794 -3600
# Node ID 7d88ebdce380fe14a4c6da51182fe551f249d162
# Parent  6f7292b946520a732ae74d7826de59e1bc8105e9
isabellesym.sty: eliminated dependency on latin1, to allow documents using utf8 instead;

diff -r 6f7292b94652 -r 7d88ebdce380 doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Thu Dec 02 21:23:56 2010 +0100
+++ b/doc-src/IsarRef/isar-ref.tex	Thu Dec 02 23:09:54 2010 +0100
@@ -1,7 +1,6 @@
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage{amssymb}
 \usepackage[greek,english]{babel}
-\usepackage[latin1]{inputenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{textcomp}
 \usepackage{latexsym}
diff -r 6f7292b94652 -r 7d88ebdce380 doc-src/isabellesym.sty
--- a/doc-src/isabellesym.sty	Thu Dec 02 21:23:56 2010 +0100
+++ b/doc-src/isabellesym.sty	Thu Dec 02 23:09:54 2010 +0100
@@ -324,12 +324,12 @@
 \newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
 \newcommand{\isasymhyphen}{\isatext{\rm-}}
 \newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}}  %requires latin1
-\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires latin1
-\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}}  %requires latin1
-\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires latin1
-\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}}  %requires latin1
-\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires latin1
+\newcommand{\isasymonesuperior}{\isamath{{}^1}}
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires textcomp
+\newcommand{\isasymtwosuperior}{\isamath{{}^2}}
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires textcomp
+\newcommand{\isasymthreesuperior}{\isamath{{}^3}}
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires textcomp
 \newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
 \newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
 \newcommand{\isasymsection}{\isatext{\rm\S}}
@@ -341,7 +341,7 @@
 \newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
 \newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
 \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
-\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires textcomp
 \newcommand{\isasymamalg}{\isamath{\amalg}}
 \newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
 \newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
diff -r 6f7292b94652 -r 7d88ebdce380 lib/Tools/latex
--- a/lib/Tools/latex	Thu Dec 02 21:23:56 2010 +0100
+++ b/lib/Tools/latex	Thu Dec 02 23:09:54 2010 +0100
@@ -88,7 +88,7 @@
 function extract_syms ()
 {
   perl -n \
-    -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
+    -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
     "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
   perl -n \
     -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
diff -r 6f7292b94652 -r 7d88ebdce380 lib/texinputs/draft.tex
--- a/lib/texinputs/draft.tex	Thu Dec 02 21:23:56 2010 +0100
+++ b/lib/texinputs/draft.tex	Thu Dec 02 23:09:54 2010 +0100
@@ -6,7 +6,6 @@
 \usepackage{isabelle,isabellesym,pdfsetup}
 
 %packages for unusual symbols according to 'isabelle latex -o syms'
-\usepackage[latin1]{inputenc}
 \usepackage{amssymb}
 \usepackage{textcomp}
 
diff -r 6f7292b94652 -r 7d88ebdce380 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Thu Dec 02 21:23:56 2010 +0100
+++ b/lib/texinputs/isabellesym.sty	Thu Dec 02 23:09:54 2010 +0100
@@ -324,12 +324,12 @@
 \newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
 \newcommand{\isasymhyphen}{\isatext{\rm-}}
 \newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}}  %requires latin1
-\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires latin1
-\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}}  %requires latin1
-\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires latin1
-\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}}  %requires latin1
-\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires latin1
+\newcommand{\isasymonesuperior}{\isamath{{}^1}}
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires textcomp
+\newcommand{\isasymtwosuperior}{\isamath{{}^2}}
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires textcomp
+\newcommand{\isasymthreesuperior}{\isamath{{}^3}}
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires textcomp
 \newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
 \newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
 \newcommand{\isasymsection}{\isatext{\rm\S}}
@@ -341,7 +341,7 @@
 \newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
 \newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
 \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
-\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires textcomp
 \newcommand{\isasymamalg}{\isamath{\amalg}}
 \newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
 \newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb