--- a/src/Doc/IsarImplementation/Eq.thy Fri Jun 21 13:36:10 2013 +0200
+++ b/src/Doc/IsarImplementation/Eq.thy Sat Jun 22 18:24:06 2013 +0200
@@ -73,7 +73,7 @@
section {* Conversions \label{sec:conv} *}
text {*
- FIXME
+ %FIXME
The classic article that introduces the concept of conversion (for
Cambridge LCF) is \cite{paulson:1983}.
--- a/src/Doc/IsarImplementation/Local_Theory.thy Fri Jun 21 13:36:10 2013 +0200
+++ b/src/Doc/IsarImplementation/Local_Theory.thy Sat Jun 22 18:24:06 2013 +0200
@@ -159,9 +159,10 @@
section {* Morphisms and declarations \label{sec:morphisms} *}
-text {* FIXME
+text {*
+ %FIXME
- \medskip See also \cite{Chaieb-Wenzel:2007}.
+ See also \cite{Chaieb-Wenzel:2007}.
*}
end
--- a/src/Doc/IsarImplementation/Logic.thy Fri Jun 21 13:36:10 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy Sat Jun 22 18:24:06 2013 +0200
@@ -1148,7 +1148,7 @@
{@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}
\]
- FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
+ %FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
*}
text %mlref {*
--- a/src/Doc/IsarImplementation/Syntax.thy Fri Jun 21 13:36:10 2013 +0200
+++ b/src/Doc/IsarImplementation/Syntax.thy Sat Jun 22 18:24:06 2013 +0200
@@ -69,11 +69,7 @@
@{index_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\
\end{mldecls}
- \begin{description}
-
- \item FIXME
-
- \end{description}
+ %FIXME description
*}
@@ -106,11 +102,7 @@
@{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
\end{mldecls}
- \begin{description}
-
- \item FIXME
-
- \end{description}
+ %FIXME description
*}
@@ -153,11 +145,7 @@
@{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
\end{mldecls}
- \begin{description}
-
- \item FIXME
-
- \end{description}
+ %FIXME description
*}
end