# HG changeset patch
# User wenzelm
# Date 1221489811 -7200
# Node ID 21f0c2de0a3805573491e8aa00ae22a3b0acf5b0
# Parent  5423ad29648e57183df5b4f69aa4d5036212a95a
added formal markup for setting, executable, tool;

diff -r 5423ad29648e -r 21f0c2de0a38 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Mon Sep 15 16:42:09 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Mon Sep 15 16:43:31 2008 +0200
@@ -198,7 +198,10 @@
   entity_antiqs no_check "" "fact" @
   entity_antiqs no_check "" "variable" @
   entity_antiqs no_check "" "case" @
-  entity_antiqs (K ThyOutput.defined_command) "" "antiquotation");
+  entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
+  entity_antiqs no_check "isatt" "setting" @
+  entity_antiqs no_check "isatt" "executable" @
+  entity_antiqs no_check "isatt" "tool");
 
 end;