# HG changeset patch
# User wenzelm
# Date 1286650159 -3600
# Node ID 350857040d09c11c7607e77831209caf8cb7bded
# Parent  7c501d7f1e45546e4dd1375af331cc905e636328
prefer checked antiquotations;

diff -r 7c501d7f1e45 -r 350857040d09 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Sat Oct 09 19:05:31 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sat Oct 09 19:49:19 2010 +0100
@@ -973,7 +973,7 @@
 
   Usually the default sort is only changed when defining a new
   object-logic.  For example, the default sort in Isabelle/HOL is
-  @{text type}, the class of all HOL types.  %FIXME sort antiq?
+  @{class type}, the class of all HOL types.
 
   When merging theories, the default sorts of the parents are
   logically intersected, i.e.\ the representations as lists of classes
diff -r 7c501d7f1e45 -r 350857040d09 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sat Oct 09 19:05:31 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sat Oct 09 19:49:19 2010 +0100
@@ -1010,7 +1010,7 @@
 
   Usually the default sort is only changed when defining a new
   object-logic.  For example, the default sort in Isabelle/HOL is
-  \isa{type}, the class of all HOL types.  %FIXME sort antiq?
+  \isa{type}, the class of all HOL types.
 
   When merging theories, the default sorts of the parents are
   logically intersected, i.e.\ the representations as lists of classes