1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Wed Jun 14 12:14:42 2006 +0200
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Wed Jun 14 12:16:49 2006 +0200
     1.3 @@ -43,13 +43,15 @@
     1.4      "classrel"
     1.5      "clear_undos"
     1.6      "code_alias"
     1.7 +    "code_classapp"
     1.8 +    "code_constapp"
     1.9      "code_generate"
    1.10      "code_library"
    1.11      "code_module"
    1.12      "code_purge"
    1.13      "code_serialize"
    1.14 -    "code_syntax_const"
    1.15 -    "code_syntax_tyco"
    1.16 +    "code_simtype"
    1.17 +    "code_typapp"
    1.18      "coinductive"
    1.19      "commit"
    1.20      "const_syntax"
    1.21 @@ -360,13 +362,14 @@
    1.22      "classes"
    1.23      "classrel"
    1.24      "code_alias"
    1.25 +    "code_classapp"
    1.26 +    "code_constapp"
    1.27      "code_generate"
    1.28      "code_library"
    1.29      "code_module"
    1.30      "code_purge"
    1.31      "code_serialize"
    1.32 -    "code_syntax_const"
    1.33 -    "code_syntax_tyco"
    1.34 +    "code_typapp"
    1.35      "coinductive"
    1.36      "const_syntax"
    1.37      "constdefs"
    1.38 @@ -424,6 +427,7 @@
    1.39  
    1.40  (defconst isar-keywords-theory-goal
    1.41    '("ax_specification"
    1.42 +    "code_simtype"
    1.43      "corollary"
    1.44      "function"
    1.45      "instance"

     2.1 --- a/etc/isar-keywords-ZF.el	Wed Jun 14 12:14:42 2006 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Wed Jun 14 12:16:49 2006 +0200
     2.3 @@ -41,13 +41,15 @@
     2.4      "clear_undos"
     2.5      "codatatype"
     2.6      "code_alias"
     2.7 +    "code_classapp"
     2.8 +    "code_constapp"
     2.9      "code_generate"
    2.10      "code_library"
    2.11      "code_module"
    2.12      "code_purge"
    2.13      "code_serialize"
    2.14 -    "code_syntax_const"
    2.15 -    "code_syntax_tyco"
    2.16 +    "code_simtype"
    2.17 +    "code_typapp"
    2.18      "coinductive"
    2.19      "commit"
    2.20      "const_syntax"
    2.21 @@ -348,13 +350,14 @@
    2.22      "classrel"
    2.23      "codatatype"
    2.24      "code_alias"
    2.25 +    "code_classapp"
    2.26 +    "code_constapp"
    2.27      "code_generate"
    2.28      "code_library"
    2.29      "code_module"
    2.30      "code_purge"
    2.31      "code_serialize"
    2.32 -    "code_syntax_const"
    2.33 -    "code_syntax_tyco"
    2.34 +    "code_typapp"
    2.35      "coinductive"
    2.36      "const_syntax"
    2.37      "constdefs"
    2.38 @@ -406,7 +409,8 @@
    2.39      "inductive_cases"))
    2.40  
    2.41  (defconst isar-keywords-theory-goal
    2.42 -  '("corollary"
    2.43 +  '("code_simtype"
    2.44 +    "corollary"
    2.45      "instance"
    2.46      "interpretation"
    2.47      "lemma"

     3.1 --- a/etc/isar-keywords.el	Wed Jun 14 12:14:42 2006 +0200
     3.2 +++ b/etc/isar-keywords.el	Wed Jun 14 12:16:49 2006 +0200
     3.3 @@ -43,13 +43,15 @@
     3.4      "classrel"
     3.5      "clear_undos"
     3.6      "code_alias"
     3.7 +    "code_classapp"
     3.8 +    "code_constapp"
     3.9      "code_generate"
    3.10      "code_library"
    3.11      "code_module"
    3.12      "code_purge"
    3.13      "code_serialize"
    3.14 -    "code_syntax_const"
    3.15 -    "code_syntax_tyco"
    3.16 +    "code_simtype"
    3.17 +    "code_typapp"
    3.18      "coinductive"
    3.19      "commit"
    3.20      "const_syntax"
    3.21 @@ -381,13 +383,14 @@
    3.22      "classes"
    3.23      "classrel"
    3.24      "code_alias"
    3.25 +    "code_classapp"
    3.26 +    "code_constapp"
    3.27      "code_generate"
    3.28      "code_library"
    3.29      "code_module"
    3.30      "code_purge"
    3.31      "code_serialize"
    3.32 -    "code_syntax_const"
    3.33 -    "code_syntax_tyco"
    3.34 +    "code_typapp"
    3.35      "coinductive"
    3.36      "const_syntax"
    3.37      "constdefs"
    3.38 @@ -447,6 +450,7 @@
    3.39  
    3.40  (defconst isar-keywords-theory-goal
    3.41    '("ax_specification"
    3.42 +    "code_simtype"
    3.43      "corollary"
    3.44      "cpodef"
    3.45      "function"