Added keywords for new inductive definition package.
authorberghofe
Fri Oct 13 18:33:50 2006 +0200 (2006-10-13)
changeset 210273f89f99d746e
parent 21026 3b2821e0d541
child 21028 ed94ba513989
Added keywords for new inductive definition package.
etc/isar-keywords.el
     1.1 --- a/etc/isar-keywords.el	Fri Oct 13 18:29:31 2006 +0200
     1.2 +++ b/etc/isar-keywords.el	Fri Oct 13 18:33:50 2006 +0200
     1.3 @@ -56,6 +56,7 @@
     1.4      "code_type"
     1.5      "code_typename"
     1.6      "coinductive"
     1.7 +    "coinductive2"
     1.8      "commit"
     1.9      "const_syntax"
    1.10      "constdefs"
    1.11 @@ -98,7 +99,9 @@
    1.12      "hence"
    1.13      "hide"
    1.14      "inductive"
    1.15 +    "inductive2"
    1.16      "inductive_cases"
    1.17 +    "inductive_cases2"
    1.18      "init_toplevel"
    1.19      "instance"
    1.20      "interpret"
    1.21 @@ -211,7 +214,6 @@
    1.22      "types_code"
    1.23      "ultimately"
    1.24      "undo"
    1.25 -    "undo_end"
    1.26      "undos_proof"
    1.27      "unfolding"
    1.28      "update_thy"
    1.29 @@ -306,7 +308,6 @@
    1.30      "quit"
    1.31      "redo"
    1.32      "undo"
    1.33 -    "undo_end"
    1.34      "undos_proof"))
    1.35  
    1.36  (defconst isar-keywords-diag
    1.37 @@ -409,6 +410,7 @@
    1.38      "code_type"
    1.39      "code_typename"
    1.40      "coinductive"
    1.41 +    "coinductive2"
    1.42      "const_syntax"
    1.43      "constdefs"
    1.44      "consts"
    1.45 @@ -428,6 +430,7 @@
    1.46      "global"
    1.47      "hide"
    1.48      "inductive"
    1.49 +    "inductive2"
    1.50      "judgment"
    1.51      "lemmas"
    1.52      "local"
    1.53 @@ -463,7 +466,8 @@
    1.54  
    1.55  (defconst isar-keywords-theory-script
    1.56    '("declare"
    1.57 -    "inductive_cases"))
    1.58 +    "inductive_cases"
    1.59 +    "inductive_cases2"))
    1.60  
    1.61  (defconst isar-keywords-theory-goal
    1.62    '("ax_specification"