added formal markup for setting, executable, tool;
authorwenzelm
Mon Sep 15 16:43:31 2008 +0200 (2008-09-15)
changeset 2821721f0c2de0a38
parent 28216 5423ad29648e
child 28218 1cb3bd5b664a
added formal markup for setting, executable, tool;
doc-src/antiquote_setup.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Mon Sep 15 16:42:09 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Mon Sep 15 16:43:31 2008 +0200
     1.3 @@ -198,7 +198,10 @@
     1.4    entity_antiqs no_check "" "fact" @
     1.5    entity_antiqs no_check "" "variable" @
     1.6    entity_antiqs no_check "" "case" @
     1.7 -  entity_antiqs (K ThyOutput.defined_command) "" "antiquotation");
     1.8 +  entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
     1.9 +  entity_antiqs no_check "isatt" "setting" @
    1.10 +  entity_antiqs no_check "isatt" "executable" @
    1.11 +  entity_antiqs no_check "isatt" "tool");
    1.12  
    1.13  end;
    1.14