--- a/doc-src/Intro/getting.tex Thu May 15 14:28:32 1997 +0200
+++ b/doc-src/Intro/getting.tex Thu May 15 14:49:41 1997 +0200
@@ -9,10 +9,6 @@
special screen font. The meta-logic and major object-logics already
provide such fancy output as an option.
-%FIXME remove
-%Menu-driven graphical interfaces are under construction, but Isabelle
-%users will always need to know some \ML, at least to use tacticals.
-
Object-logics are built upon Pure Isabelle, which implements the
meta-logic and provides certain fundamental data structures: types,
terms, signatures, theorems and theories, tactics and tacticals.