etc/isar-keywords.el
changeset 24343 acc0f7aac619
parent 24249 1f60b45c5f97
child 24437 c2a76e8a3d54
equal deleted inserted replaced
24342:a1d489e254ec 24343:acc0f7aac619
    42     "code_axioms"
    42     "code_axioms"
    43     "code_class"
    43     "code_class"
    44     "code_const"
    44     "code_const"
    45     "code_datatype"
    45     "code_datatype"
    46     "code_deps"
    46     "code_deps"
    47     "code_gen"
       
    48     "code_instance"
    47     "code_instance"
    49     "code_library"
    48     "code_library"
    50     "code_module"
    49     "code_module"
    51     "code_modulename"
    50     "code_modulename"
    52     "code_moduleprolog"
    51     "code_moduleprolog"
    77     "domain"
    76     "domain"
    78     "done"
    77     "done"
    79     "enable_pr"
    78     "enable_pr"
    80     "end"
    79     "end"
    81     "exit"
    80     "exit"
       
    81     "export_code"
    82     "extract"
    82     "extract"
    83     "extract_type"
    83     "extract_type"
    84     "finalconsts"
    84     "finalconsts"
    85     "finally"
    85     "finally"
    86     "find_theorems"
    86     "find_theorems"
   153     "print_induct_rules"
   153     "print_induct_rules"
   154     "print_interps"
   154     "print_interps"
   155     "print_locale"
   155     "print_locale"
   156     "print_locales"
   156     "print_locales"
   157     "print_methods"
   157     "print_methods"
       
   158     "print_noatp_rules"
   158     "print_rules"
   159     "print_rules"
   159     "print_simpset"
   160     "print_simpset"
   160     "print_statement"
   161     "print_statement"
   161     "print_syntax"
   162     "print_syntax"
   162     "print_theorems"
   163     "print_theorems"
   204     "thm"
   205     "thm"
   205     "thm_deps"
   206     "thm_deps"
   206     "thus"
   207     "thus"
   207     "thy_deps"
   208     "thy_deps"
   208     "token_translation"
   209     "token_translation"
   209     "touch_all_thys"
       
   210     "touch_child_thys"
   210     "touch_child_thys"
   211     "touch_thy"
   211     "touch_thy"
   212     "translations"
   212     "translations"
   213     "txt"
   213     "txt"
   214     "txt_raw"
   214     "txt_raw"
   313   '("ML"
   313   '("ML"
   314     "ML_command"
   314     "ML_command"
   315     "cd"
   315     "cd"
   316     "class_deps"
   316     "class_deps"
   317     "code_deps"
   317     "code_deps"
   318     "code_gen"
       
   319     "code_thms"
   318     "code_thms"
   320     "commit"
   319     "commit"
   321     "disable_pr"
   320     "disable_pr"
   322     "display_drafts"
   321     "display_drafts"
   323     "enable_pr"
   322     "enable_pr"
       
   323     "export_code"
   324     "find_theorems"
   324     "find_theorems"
   325     "full_prf"
   325     "full_prf"
   326     "header"
   326     "header"
   327     "help"
   327     "help"
   328     "kill_thy"
   328     "kill_thy"
   347     "print_induct_rules"
   347     "print_induct_rules"
   348     "print_interps"
   348     "print_interps"
   349     "print_locale"
   349     "print_locale"
   350     "print_locales"
   350     "print_locales"
   351     "print_methods"
   351     "print_methods"
       
   352     "print_noatp_rules"
   352     "print_rules"
   353     "print_rules"
   353     "print_simpset"
   354     "print_simpset"
   354     "print_statement"
   355     "print_statement"
   355     "print_syntax"
   356     "print_syntax"
   356     "print_theorems"
   357     "print_theorems"
   364     "sledgehammer"
   365     "sledgehammer"
   365     "term"
   366     "term"
   366     "thm"
   367     "thm"
   367     "thm_deps"
   368     "thm_deps"
   368     "thy_deps"
   369     "thy_deps"
   369     "touch_all_thys"
       
   370     "touch_child_thys"
   370     "touch_child_thys"
   371     "touch_thy"
   371     "touch_thy"
   372     "typ"
   372     "typ"
   373     "use"
   373     "use"
   374     "use_thy"
   374     "use_thy"