update the keywords files
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 22 Feb 2010 10:28:49 +0100
changeset 352794f6760122b2a
parent 35278 a5d0bfcaf26a
child 35280 54ab4921f826
child 35298 71bca9e4c483
child 35299 4f4d5bf4ea08
update the keywords files
etc/isar-keywords-ZF.el
etc/isar-keywords.el
     1.1 --- a/etc/isar-keywords-ZF.el	Mon Feb 22 10:28:00 2010 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon Feb 22 10:28:49 2010 +0100
     1.3 @@ -44,6 +44,7 @@
     1.4      "classes"
     1.5      "classrel"
     1.6      "codatatype"
     1.7 +    "code_abstype"
     1.8      "code_datatype"
     1.9      "code_library"
    1.10      "code_module"
    1.11 @@ -413,7 +414,8 @@
    1.12    '("inductive_cases"))
    1.13  
    1.14  (defconst isar-keywords-theory-goal
    1.15 -  '("corollary"
    1.16 +  '("code_abstype"
    1.17 +    "corollary"
    1.18      "instance"
    1.19      "interpretation"
    1.20      "lemma"
     2.1 --- a/etc/isar-keywords.el	Mon Feb 22 10:28:00 2010 +0100
     2.2 +++ b/etc/isar-keywords.el	Mon Feb 22 10:28:49 2010 +0100
     2.3 @@ -188,6 +188,9 @@
     2.4      "print_locales"
     2.5      "print_methods"
     2.6      "print_orders"
     2.7 +    "print_quotconsts"
     2.8 +    "print_quotients"
     2.9 +    "print_quotmaps"
    2.10      "print_rules"
    2.11      "print_simpset"
    2.12      "print_statement"
    2.13 @@ -203,6 +206,8 @@
    2.14      "quickcheck"
    2.15      "quickcheck_params"
    2.16      "quit"
    2.17 +    "quotient_definition"
    2.18 +    "quotient_type"
    2.19      "realizability"
    2.20      "realizers"
    2.21      "recdef"
    2.22 @@ -395,6 +400,9 @@
    2.23      "print_locales"
    2.24      "print_methods"
    2.25      "print_orders"
    2.26 +    "print_quotconsts"
    2.27 +    "print_quotients"
    2.28 +    "print_quotmaps"
    2.29      "print_rules"
    2.30      "print_simpset"
    2.31      "print_statement"
    2.32 @@ -512,6 +520,7 @@
    2.33      "print_ast_translation"
    2.34      "print_translation"
    2.35      "quickcheck_params"
    2.36 +    "quotient_definition"
    2.37      "realizability"
    2.38      "realizers"
    2.39      "recdef"
    2.40 @@ -550,6 +559,7 @@
    2.41      "nominal_inductive2"
    2.42      "nominal_primrec"
    2.43      "pcpodef"
    2.44 +    "quotient_type"
    2.45      "recdef_tc"
    2.46      "rep_datatype"
    2.47      "specification"