src/Doc/antiquote_setup.ML
changeset 69962 82e945d472d5
parent 69593 3dda49e08b9d
child 70121 61e26527480e
equal deleted inserted replaced
69961:708743578e45 69962:82e945d472d5
   194     entity_antiqs no_check "" \<^binding>\<open>fact\<close> #>
   194     entity_antiqs no_check "" \<^binding>\<open>fact\<close> #>
   195     entity_antiqs no_check "" \<^binding>\<open>variable\<close> #>
   195     entity_antiqs no_check "" \<^binding>\<open>variable\<close> #>
   196     entity_antiqs no_check "" \<^binding>\<open>case\<close> #>
   196     entity_antiqs no_check "" \<^binding>\<open>case\<close> #>
   197     entity_antiqs Document_Antiquotation.check "" \<^binding>\<open>antiquotation\<close> #>
   197     entity_antiqs Document_Antiquotation.check "" \<^binding>\<open>antiquotation\<close> #>
   198     entity_antiqs Document_Antiquotation.check_option "" \<^binding>\<open>antiquotation_option\<close> #>
   198     entity_antiqs Document_Antiquotation.check_option "" \<^binding>\<open>antiquotation_option\<close> #>
       
   199     entity_antiqs Document_Marker.check "" \<^binding>\<open>document_marker\<close> #>
   199     entity_antiqs no_check "isasystem" \<^binding>\<open>setting\<close> #>
   200     entity_antiqs no_check "isasystem" \<^binding>\<open>setting\<close> #>
   200     entity_antiqs check_system_option "isasystem" \<^binding>\<open>system_option\<close> #>
   201     entity_antiqs check_system_option "isasystem" \<^binding>\<open>system_option\<close> #>
   201     entity_antiqs no_check "" \<^binding>\<open>inference\<close> #>
   202     entity_antiqs no_check "" \<^binding>\<open>inference\<close> #>
   202     entity_antiqs no_check "isasystem" \<^binding>\<open>executable\<close> #>
   203     entity_antiqs no_check "isasystem" \<^binding>\<open>executable\<close> #>
   203     entity_antiqs no_check "isatool" \<^binding>\<open>tool\<close> #>
   204     entity_antiqs no_check "isatool" \<^binding>\<open>tool\<close> #>