# HG changeset patch
# User wenzelm
# Date 1451412683 -3600
# Node ID 9c8fc56032e3618f5bd57217cfa99debb54a7a2f
# Parent  c4cc05200337fcc86e3198610831e87febed0d48
eliminated obscure macro that is in conflict with amsmath.sty;

diff -r c4cc05200337 -r 9c8fc56032e3 src/Doc/Eisbach/document/style.sty
--- a/src/Doc/Eisbach/document/style.sty	Tue Dec 29 17:54:45 2015 +0100
+++ b/src/Doc/Eisbach/document/style.sty	Tue Dec 29 19:11:23 2015 +0100
@@ -8,7 +8,6 @@
 \newcommand{\figref}[1]{figure~\ref{#1}}
 
 %% math
-\newcommand{\text}[1]{\mbox{#1}}
 \newcommand{\isasymvartheta}{\isamath{\theta}}
 \newcommand{\isactrlvec}[1]{\emph{$\vec{#1}$}}
 \newcommand{\isactrlBG}{\isacharbackquoteopen}
diff -r c4cc05200337 -r 9c8fc56032e3 src/Doc/Functions/document/style.sty
--- a/src/Doc/Functions/document/style.sty	Tue Dec 29 17:54:45 2015 +0100
+++ b/src/Doc/Functions/document/style.sty	Tue Dec 29 19:11:23 2015 +0100
@@ -8,7 +8,6 @@
 \newcommand{\figref}[1]{figure~\ref{#1}}
 
 %% math
-\newcommand{\text}[1]{\mbox{#1}}
 \newcommand{\isasymvartheta}{\isamath{\theta}}
 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
 
diff -r c4cc05200337 -r 9c8fc56032e3 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Tue Dec 29 17:54:45 2015 +0100
+++ b/src/Doc/Implementation/Logic.thy	Tue Dec 29 19:11:23 2015 +0100
@@ -1011,7 +1011,7 @@
   (again modulo unification):
   \[
   \infer[(@{inference_def assumption})]{\<open>C\<vartheta>\<close>}
-  {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\text{(for some~\<open>i\<close>)}}
+  {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\mbox{(for some~\<open>i\<close>)}}
   \]
 
   %FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
diff -r c4cc05200337 -r 9c8fc56032e3 src/Doc/Implementation/document/style.sty
--- a/src/Doc/Implementation/document/style.sty	Tue Dec 29 17:54:45 2015 +0100
+++ b/src/Doc/Implementation/document/style.sty	Tue Dec 29 19:11:23 2015 +0100
@@ -8,7 +8,6 @@
 \newcommand{\figref}[1]{figure~\ref{#1}}
 
 %% math
-\newcommand{\text}[1]{\mbox{#1}}
 \newcommand{\isasymvartheta}{\isamath{\theta}}
 \newcommand{\isactrlvec}[1]{\emph{$\vec{#1}$}}
 \newcommand{\isactrlBG}{\isacharbackquoteopen}
diff -r c4cc05200337 -r 9c8fc56032e3 src/Doc/Isar_Ref/Framework.thy
--- a/src/Doc/Isar_Ref/Framework.thy	Tue Dec 29 17:54:45 2015 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy	Tue Dec 29 19:11:23 2015 +0100
@@ -283,7 +283,7 @@
   collection of axioms:
 
   \[
-  \infer{\<open>\<turnstile> A\<close>}{(\<open>A\<close> \text{~axiom})}
+  \infer{\<open>\<turnstile> A\<close>}{(\<open>A\<close> \mbox{~axiom})}
   \qquad
   \infer{\<open>A \<turnstile> A\<close>}{}
   \]
@@ -397,7 +397,7 @@
   {\begin{tabular}{rl}
     \<open>goal:\<close> &
     \<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> \\
-    \<open>assm unifier:\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\text{(for some~\<open>H\<^sub>i\<close>)} \\
+    \<open>assm unifier:\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\mbox{(for some~\<open>H\<^sub>i\<close>)} \\
    \end{tabular}}
   \]
 
diff -r c4cc05200337 -r 9c8fc56032e3 src/Doc/Isar_Ref/document/style.sty
--- a/src/Doc/Isar_Ref/document/style.sty	Tue Dec 29 17:54:45 2015 +0100
+++ b/src/Doc/Isar_Ref/document/style.sty	Tue Dec 29 19:11:23 2015 +0100
@@ -30,7 +30,6 @@
 \newcommand{\isasymvartheta}{\isamath{\,\theta}}
 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
 \renewcommand{\isadigit}[1]{\isamath{#1}}
-\newcommand{\text}[1]{\mbox{#1}}
 
 %% global style options
 \pagestyle{headings}