equal
deleted
inserted
replaced
199 entity_antiqs Document_Marker.check "" \<^binding>\<open>document_marker\<close> #> |
199 entity_antiqs Document_Marker.check "" \<^binding>\<open>document_marker\<close> #> |
200 entity_antiqs no_check "isasystem" \<^binding>\<open>setting\<close> #> |
200 entity_antiqs no_check "isasystem" \<^binding>\<open>setting\<close> #> |
201 entity_antiqs check_system_option "isasystem" \<^binding>\<open>system_option\<close> #> |
201 entity_antiqs check_system_option "isasystem" \<^binding>\<open>system_option\<close> #> |
202 entity_antiqs no_check "" \<^binding>\<open>inference\<close> #> |
202 entity_antiqs no_check "" \<^binding>\<open>inference\<close> #> |
203 entity_antiqs no_check "isasystem" \<^binding>\<open>executable\<close> #> |
203 entity_antiqs no_check "isasystem" \<^binding>\<open>executable\<close> #> |
204 entity_antiqs no_check "isatool" \<^binding>\<open>tool\<close> #> |
204 entity_antiqs Isabelle_Tool.check "isatool" \<^binding>\<open>tool\<close> #> |
205 entity_antiqs ML_Context.check_antiquotation "" \<^binding>\<open>ML_antiquotation\<close> #> |
205 entity_antiqs ML_Context.check_antiquotation "" \<^binding>\<open>ML_antiquotation\<close> #> |
206 entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\<open>action\<close>); |
206 entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\<open>action\<close>); |
207 |
207 |
208 end; |
208 end; |
209 |
209 |