# HG changeset patch
# User wenzelm
# Date 1371918246 -7200
# Node ID 93f3f9a2ae91ce66fde53591ff8ee612d1113afb
# Parent  6d93140a206cb1c4800d0d4305abf731149558ca
tuned;

diff -r 6d93140a206c -r 93f3f9a2ae91 src/Doc/IsarImplementation/Eq.thy
--- 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}.
diff -r 6d93140a206c -r 93f3f9a2ae91 src/Doc/IsarImplementation/Local_Theory.thy
--- 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
diff -r 6d93140a206c -r 93f3f9a2ae91 src/Doc/IsarImplementation/Logic.thy
--- 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 {*
diff -r 6d93140a206c -r 93f3f9a2ae91 src/Doc/IsarImplementation/Syntax.thy
--- 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