# HG changeset patch # User wenzelm # Date 1234384777 -3600 # Node ID 5f91ff5c03a2792ac9c99780797ae90a3b4f76f5 # Parent 03916d2d16d33aa42e00373f502bea2a96f3e976 added "inference" entity; diff -r 03916d2d16d3 -r 5f91ff5c03a2 doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Wed Feb 11 21:39:12 2009 +0100 +++ b/doc-src/antiquote_setup.ML Wed Feb 11 21:39:37 2009 +0100 @@ -1,5 +1,4 @@ (* Title: Doc/antiquote_setup.ML - ID: $Id$ Author: Makarius Auxiliary antiquotations for the Isabelle manuals. @@ -193,6 +192,7 @@ entity_antiqs no_check "" "case" @ entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @ entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @ + entity_antiqs no_check "" "inference" @ entity_antiqs no_check "isatt" "executable" @ entity_antiqs (K check_tool) "isatt" "tool" @ entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @