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"