Adapted to changes in inductive definition package.
authorberghofe
Wed Jul 11 10:52:20 2007 +0200 (2007-07-11)
changeset 23732f9f89b7cfdc7
parent 23731 e42f71809a7a
child 23733 3f8ad7418e55
Adapted to changes in inductive definition package.
etc/isar-keywords-HOL-Nominal.el
etc/isar-keywords.el
     1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Wed Jul 11 00:46:48 2007 +0200
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Wed Jul 11 10:52:20 2007 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4      "code_thms"
     1.5      "code_type"
     1.6      "coinductive"
     1.7 -    "coinductive2"
     1.8 +    "coinductive_set"
     1.9      "commit"
    1.10      "constdefs"
    1.11      "consts"
    1.12 @@ -96,9 +96,8 @@
    1.13      "hence"
    1.14      "hide"
    1.15      "inductive"
    1.16 -    "inductive2"
    1.17      "inductive_cases"
    1.18 -    "inductive_cases2"
    1.19 +    "inductive_set"
    1.20      "init_toplevel"
    1.21      "instance"
    1.22      "interpret"
    1.23 @@ -261,7 +260,6 @@
    1.24      "infixl"
    1.25      "infixr"
    1.26      "inject"
    1.27 -    "intros"
    1.28      "invariant"
    1.29      "is"
    1.30      "monos"
    1.31 @@ -404,7 +402,7 @@
    1.32      "code_reserved"
    1.33      "code_type"
    1.34      "coinductive"
    1.35 -    "coinductive2"
    1.36 +    "coinductive_set"
    1.37      "constdefs"
    1.38      "consts"
    1.39      "consts_code"
    1.40 @@ -423,7 +421,7 @@
    1.41      "global"
    1.42      "hide"
    1.43      "inductive"
    1.44 -    "inductive2"
    1.45 +    "inductive_set"
    1.46      "judgment"
    1.47      "lemmas"
    1.48      "local"
    1.49 @@ -462,8 +460,7 @@
    1.50  
    1.51  (defconst isar-keywords-theory-script
    1.52    '("declare"
    1.53 -    "inductive_cases"
    1.54 -    "inductive_cases2"))
    1.55 +    "inductive_cases"))
    1.56  
    1.57  (defconst isar-keywords-theory-goal
    1.58    '("ax_specification"
     2.1 --- a/etc/isar-keywords.el	Wed Jul 11 00:46:48 2007 +0200
     2.2 +++ b/etc/isar-keywords.el	Wed Jul 11 10:52:20 2007 +0200
     2.3 @@ -55,7 +55,7 @@
     2.4      "code_thms"
     2.5      "code_type"
     2.6      "coinductive"
     2.7 -    "coinductive2"
     2.8 +    "coinductive_set"
     2.9      "commit"
    2.10      "constdefs"
    2.11      "consts"
    2.12 @@ -99,9 +99,8 @@
    2.13      "hence"
    2.14      "hide"
    2.15      "inductive"
    2.16 -    "inductive2"
    2.17      "inductive_cases"
    2.18 -    "inductive_cases2"
    2.19 +    "inductive_set"
    2.20      "init_toplevel"
    2.21      "instance"
    2.22      "interpret"
    2.23 @@ -266,7 +265,6 @@
    2.24      "inject"
    2.25      "inputs"
    2.26      "internals"
    2.27 -    "intros"
    2.28      "is"
    2.29      "lazy"
    2.30      "monos"
    2.31 @@ -418,7 +416,7 @@
    2.32      "code_reserved"
    2.33      "code_type"
    2.34      "coinductive"
    2.35 -    "coinductive2"
    2.36 +    "coinductive_set"
    2.37      "constdefs"
    2.38      "consts"
    2.39      "consts_code"
    2.40 @@ -439,7 +437,7 @@
    2.41      "global"
    2.42      "hide"
    2.43      "inductive"
    2.44 -    "inductive2"
    2.45 +    "inductive_set"
    2.46      "judgment"
    2.47      "lemmas"
    2.48      "local"
    2.49 @@ -477,8 +475,7 @@
    2.50  
    2.51  (defconst isar-keywords-theory-script
    2.52    '("declare"
    2.53 -    "inductive_cases"
    2.54 -    "inductive_cases2"))
    2.55 +    "inductive_cases"))
    2.56  
    2.57  (defconst isar-keywords-theory-goal
    2.58    '("ax_specification"