1.1 --- a/etc/isar-keywords-ZF.el	Mon Oct 08 18:13:01 2007 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon Oct 08 18:13:03 2007 +0200
     1.3 @@ -1,6 +1,7 @@
     1.4  ;;
     1.5  ;; Keyword classification tables for Isabelle/Isar.
     1.6 -;; This file was generated from FOL + ZF -- DO NOT EDIT!
     1.7 +;; Generated from Pure + Pure-ProofGeneral + FOL + ZF
     1.8 +;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     1.9  ;;
    1.10  ;; $Id$
    1.11  ;;

     2.1 --- a/etc/isar-keywords.el	Mon Oct 08 18:13:01 2007 +0200
     2.2 +++ b/etc/isar-keywords.el	Mon Oct 08 18:13:03 2007 +0200
     2.3 @@ -1,6 +1,7 @@
     2.4  ;;
     2.5  ;; Keyword classification tables for Isabelle/Isar.
     2.6 -;; This file was generated from HOL + HOLCF + IOA -- DO NOT EDIT!
     2.7 +;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal
     2.8 +;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     2.9  ;;
    2.10  ;; $Id$
    2.11  ;;
    2.12 @@ -23,6 +24,7 @@
    2.13      "apply_end"
    2.14      "arities"
    2.15      "assume"
    2.16 +    "atom_decl"
    2.17      "automaton"
    2.18      "ax_specification"
    2.19      "axclass"
    2.20 @@ -77,6 +79,7 @@
    2.21      "done"
    2.22      "enable_pr"
    2.23      "end"
    2.24 +    "equivariance"
    2.25      "exit"
    2.26      "export_code"
    2.27      "extract"
    2.28 @@ -121,6 +124,9 @@
    2.29      "next"
    2.30      "no_syntax"
    2.31      "no_translations"
    2.32 +    "nominal_datatype"
    2.33 +    "nominal_inductive"
    2.34 +    "nominal_primrec"
    2.35      "nonterminals"
    2.36      "normal_form"
    2.37      "notation"
    2.38 @@ -240,6 +246,7 @@
    2.39      "and"
    2.40      "assumes"
    2.41      "attach"
    2.42 +    "avoids"
    2.43      "begin"
    2.44      "binder"
    2.45      "compose"
    2.46 @@ -399,6 +406,7 @@
    2.47    '("ML_setup"
    2.48      "abbreviation"
    2.49      "arities"
    2.50 +    "atom_decl"
    2.51      "automaton"
    2.52      "axclass"
    2.53      "axiomatization"
    2.54 @@ -433,6 +441,7 @@
    2.55      "definition"
    2.56      "defs"
    2.57      "domain"
    2.58 +    "equivariance"
    2.59      "extract"
    2.60      "extract_type"
    2.61      "finalconsts"
    2.62 @@ -451,6 +460,7 @@
    2.63      "method_setup"
    2.64      "no_syntax"
    2.65      "no_translations"
    2.66 +    "nominal_datatype"
    2.67      "nonterminals"
    2.68      "notation"
    2.69      "oracle"
    2.70 @@ -491,6 +501,8 @@
    2.71      "instance_proof"
    2.72      "interpretation"
    2.73      "lemma"
    2.74 +    "nominal_inductive"
    2.75 +    "nominal_primrec"
    2.76      "pcpodef"
    2.77      "recdef_tc"
    2.78      "specification"

     3.1 --- a/lib/jedit/isabelle.xml	Mon Oct 08 18:13:01 2007 +0200
     3.2 +++ b/lib/jedit/isabelle.xml	Mon Oct 08 18:13:03 2007 +0200
     3.3 @@ -1,6 +1,7 @@
     3.4  <?xml version="1.0"?>
     3.5  <!DOCTYPE MODE SYSTEM "xmode.dtd">
     3.6 -<!-- This file was generated from Pure + HOL + HOLCF + IOA + HOL-Nominal + FOL + ZF -->
     3.7 +<!-- Generated from Pure + HOL + HOLCF + IOA + HOL-Nominal + FOL + ZF -->
     3.8 +<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->
     3.9  <MODE>
    3.10    <PROPS>
    3.11      <PROPERTY NAME="commentStart" VALUE="(*"/>
    3.12 @@ -131,7 +132,6 @@
    3.13        <OPERATOR>fixpat</OPERATOR>
    3.14        <OPERATOR>fixrec</OPERATOR>
    3.15        <KEYWORD4>for</KEYWORD4>
    3.16 -      <KEYWORD4>freshness_context</KEYWORD4>
    3.17        <OPERATOR>from</OPERATOR>
    3.18        <LABEL>full_prf</LABEL>
    3.19        <OPERATOR>fun</OPERATOR>
    3.20 @@ -168,7 +168,6 @@
    3.21        <OPERATOR>interpret</OPERATOR>
    3.22        <OPERATOR>interpretation</OPERATOR>
    3.23        <KEYWORD4>intros</KEYWORD4>
    3.24 -      <KEYWORD4>invariant</KEYWORD4>
    3.25        <OPERATOR>invoke</OPERATOR>
    3.26        <KEYWORD4>is</KEYWORD4>
    3.27        <OPERATOR>judgment</OPERATOR>