updated keywords
authorhaftmann
Mon Aug 20 18:07:26 2007 +0200 (2007-08-20)
changeset 24343acc0f7aac619
parent 24342 a1d489e254ec
child 24344 a0fd8c2db293
updated keywords
etc/isar-keywords-HOL-Nominal.el
etc/isar-keywords-ZF.el
etc/isar-keywords.el
     1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Mon Aug 20 18:07:25 2007 +0200
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Mon Aug 20 18:07:26 2007 +0200
     1.3 @@ -44,7 +44,6 @@
     1.4      "code_const"
     1.5      "code_datatype"
     1.6      "code_deps"
     1.7 -    "code_gen"
     1.8      "code_instance"
     1.9      "code_library"
    1.10      "code_module"
    1.11 @@ -78,6 +77,7 @@
    1.12      "end"
    1.13      "equivariance"
    1.14      "exit"
    1.15 +    "export_code"
    1.16      "extract"
    1.17      "extract_type"
    1.18      "finalconsts"
    1.19 @@ -154,6 +154,7 @@
    1.20      "print_locale"
    1.21      "print_locales"
    1.22      "print_methods"
    1.23 +    "print_noatp_rules"
    1.24      "print_rules"
    1.25      "print_simpset"
    1.26      "print_statement"
    1.27 @@ -205,7 +206,6 @@
    1.28      "thus"
    1.29      "thy_deps"
    1.30      "token_translation"
    1.31 -    "touch_all_thys"
    1.32      "touch_child_thys"
    1.33      "touch_thy"
    1.34      "translations"
    1.35 @@ -300,12 +300,12 @@
    1.36      "cd"
    1.37      "class_deps"
    1.38      "code_deps"
    1.39 -    "code_gen"
    1.40      "code_thms"
    1.41      "commit"
    1.42      "disable_pr"
    1.43      "display_drafts"
    1.44      "enable_pr"
    1.45 +    "export_code"
    1.46      "find_theorems"
    1.47      "full_prf"
    1.48      "header"
    1.49 @@ -334,6 +334,7 @@
    1.50      "print_locale"
    1.51      "print_locales"
    1.52      "print_methods"
    1.53 +    "print_noatp_rules"
    1.54      "print_rules"
    1.55      "print_simpset"
    1.56      "print_statement"
    1.57 @@ -351,7 +352,6 @@
    1.58      "thm"
    1.59      "thm_deps"
    1.60      "thy_deps"
    1.61 -    "touch_all_thys"
    1.62      "touch_child_thys"
    1.63      "touch_thy"
    1.64      "typ"
     2.1 --- a/etc/isar-keywords-ZF.el	Mon Aug 20 18:07:25 2007 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Mon Aug 20 18:07:26 2007 +0200
     2.3 @@ -37,27 +37,11 @@
     2.4      "classes"
     2.5      "classrel"
     2.6      "codatatype"
     2.7 -    "code_abstype"
     2.8 -    "code_axioms"
     2.9 -    "code_class"
    2.10 -    "code_const"
    2.11      "code_datatype"
    2.12 -    "code_deps"
    2.13 -    "code_gen"
    2.14 -    "code_instance"
    2.15 -    "code_library"
    2.16 -    "code_module"
    2.17 -    "code_modulename"
    2.18 -    "code_moduleprolog"
    2.19 -    "code_monad"
    2.20 -    "code_reserved"
    2.21 -    "code_thms"
    2.22 -    "code_type"
    2.23      "coinductive"
    2.24      "commit"
    2.25      "constdefs"
    2.26      "consts"
    2.27 -    "consts_code"
    2.28      "context"
    2.29      "corollary"
    2.30      "datatype"
    2.31 @@ -155,8 +139,6 @@
    2.32      "prop"
    2.33      "pwd"
    2.34      "qed"
    2.35 -    "quickcheck"
    2.36 -    "quickcheck_params"
    2.37      "quit"
    2.38      "realizability"
    2.39      "realizers"
    2.40 @@ -186,7 +168,6 @@
    2.41      "thus"
    2.42      "thy_deps"
    2.43      "token_translation"
    2.44 -    "touch_all_thys"
    2.45      "touch_child_thys"
    2.46      "touch_thy"
    2.47      "translations"
    2.48 @@ -196,7 +177,6 @@
    2.49      "typed_print_translation"
    2.50      "typedecl"
    2.51      "types"
    2.52 -    "types_code"
    2.53      "ultimately"
    2.54      "undo"
    2.55      "undos_proof"
    2.56 @@ -204,7 +184,6 @@
    2.57      "use"
    2.58      "use_thy"
    2.59      "using"
    2.60 -    "value"
    2.61      "welcome"
    2.62      "with"
    2.63      "{"
    2.64 @@ -221,11 +200,9 @@
    2.65      "con_defs"
    2.66      "concl"
    2.67      "constrains"
    2.68 -    "contains"
    2.69      "defines"
    2.70      "domains"
    2.71      "elimination"
    2.72 -    "file"
    2.73      "fixes"
    2.74      "for"
    2.75      "identifier"
    2.76 @@ -239,7 +216,6 @@
    2.77      "infixr"
    2.78      "intros"
    2.79      "is"
    2.80 -    "module_name"
    2.81      "monos"
    2.82      "notes"
    2.83      "obtains"
    2.84 @@ -276,9 +252,6 @@
    2.85      "ML_command"
    2.86      "cd"
    2.87      "class_deps"
    2.88 -    "code_deps"
    2.89 -    "code_gen"
    2.90 -    "code_thms"
    2.91      "commit"
    2.92      "disable_pr"
    2.93      "display_drafts"
    2.94 @@ -319,19 +292,16 @@
    2.95      "print_trans_rules"
    2.96      "prop"
    2.97      "pwd"
    2.98 -    "quickcheck"
    2.99      "remove_thy"
   2.100      "term"
   2.101      "thm"
   2.102      "thm_deps"
   2.103      "thy_deps"
   2.104 -    "touch_all_thys"
   2.105      "touch_child_thys"
   2.106      "touch_thy"
   2.107      "typ"
   2.108      "use"
   2.109      "use_thy"
   2.110 -    "value"
   2.111      "welcome"))
   2.112  
   2.113  (defconst isar-keywords-theory-begin
   2.114 @@ -360,23 +330,10 @@
   2.115      "classes"
   2.116      "classrel"
   2.117      "codatatype"
   2.118 -    "code_abstype"
   2.119 -    "code_axioms"
   2.120 -    "code_class"
   2.121 -    "code_const"
   2.122      "code_datatype"
   2.123 -    "code_instance"
   2.124 -    "code_library"
   2.125 -    "code_module"
   2.126 -    "code_modulename"
   2.127 -    "code_moduleprolog"
   2.128 -    "code_monad"
   2.129 -    "code_reserved"
   2.130 -    "code_type"
   2.131      "coinductive"
   2.132      "constdefs"
   2.133      "consts"
   2.134 -    "consts_code"
   2.135      "context"
   2.136      "datatype"
   2.137      "declaration"
   2.138 @@ -405,7 +362,6 @@
   2.139      "primrec"
   2.140      "print_ast_translation"
   2.141      "print_translation"
   2.142 -    "quickcheck_params"
   2.143      "realizability"
   2.144      "realizers"
   2.145      "rep_datatype"
   2.146 @@ -419,8 +375,7 @@
   2.147      "translations"
   2.148      "typed_print_translation"
   2.149      "typedecl"
   2.150 -    "types"
   2.151 -    "types_code"))
   2.152 +    "types"))
   2.153  
   2.154  (defconst isar-keywords-theory-script
   2.155    '("inductive_cases"))
     3.1 --- a/etc/isar-keywords.el	Mon Aug 20 18:07:25 2007 +0200
     3.2 +++ b/etc/isar-keywords.el	Mon Aug 20 18:07:26 2007 +0200
     3.3 @@ -44,7 +44,6 @@
     3.4      "code_const"
     3.5      "code_datatype"
     3.6      "code_deps"
     3.7 -    "code_gen"
     3.8      "code_instance"
     3.9      "code_library"
    3.10      "code_module"
    3.11 @@ -79,6 +78,7 @@
    3.12      "enable_pr"
    3.13      "end"
    3.14      "exit"
    3.15 +    "export_code"
    3.16      "extract"
    3.17      "extract_type"
    3.18      "finalconsts"
    3.19 @@ -155,6 +155,7 @@
    3.20      "print_locale"
    3.21      "print_locales"
    3.22      "print_methods"
    3.23 +    "print_noatp_rules"
    3.24      "print_rules"
    3.25      "print_simpset"
    3.26      "print_statement"
    3.27 @@ -206,7 +207,6 @@
    3.28      "thus"
    3.29      "thy_deps"
    3.30      "token_translation"
    3.31 -    "touch_all_thys"
    3.32      "touch_child_thys"
    3.33      "touch_thy"
    3.34      "translations"
    3.35 @@ -315,12 +315,12 @@
    3.36      "cd"
    3.37      "class_deps"
    3.38      "code_deps"
    3.39 -    "code_gen"
    3.40      "code_thms"
    3.41      "commit"
    3.42      "disable_pr"
    3.43      "display_drafts"
    3.44      "enable_pr"
    3.45 +    "export_code"
    3.46      "find_theorems"
    3.47      "full_prf"
    3.48      "header"
    3.49 @@ -349,6 +349,7 @@
    3.50      "print_locale"
    3.51      "print_locales"
    3.52      "print_methods"
    3.53 +    "print_noatp_rules"
    3.54      "print_rules"
    3.55      "print_simpset"
    3.56      "print_statement"
    3.57 @@ -366,7 +367,6 @@
    3.58      "thm"
    3.59      "thm_deps"
    3.60      "thy_deps"
    3.61 -    "touch_all_thys"
    3.62      "touch_child_thys"
    3.63      "touch_thy"
    3.64      "typ"