--- a/etc/isar-keywords-ZF.el Mon Oct 08 18:13:01 2007 +0200
+++ b/etc/isar-keywords-ZF.el Mon Oct 08 18:13:03 2007 +0200
@@ -1,6 +1,7 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; This file was generated from FOL + ZF -- DO NOT EDIT!
+;; Generated from Pure + Pure-ProofGeneral + FOL + ZF
+;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
;; $Id$
;;
--- a/etc/isar-keywords.el Mon Oct 08 18:13:01 2007 +0200
+++ b/etc/isar-keywords.el Mon Oct 08 18:13:03 2007 +0200
@@ -1,6 +1,7 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; This file was generated from HOL + HOLCF + IOA -- DO NOT EDIT!
+;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal
+;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
;; $Id$
;;
@@ -23,6 +24,7 @@
"apply_end"
"arities"
"assume"
+ "atom_decl"
"automaton"
"ax_specification"
"axclass"
@@ -77,6 +79,7 @@
"done"
"enable_pr"
"end"
+ "equivariance"
"exit"
"export_code"
"extract"
@@ -121,6 +124,9 @@
"next"
"no_syntax"
"no_translations"
+ "nominal_datatype"
+ "nominal_inductive"
+ "nominal_primrec"
"nonterminals"
"normal_form"
"notation"
@@ -240,6 +246,7 @@
"and"
"assumes"
"attach"
+ "avoids"
"begin"
"binder"
"compose"
@@ -399,6 +406,7 @@
'("ML_setup"
"abbreviation"
"arities"
+ "atom_decl"
"automaton"
"axclass"
"axiomatization"
@@ -433,6 +441,7 @@
"definition"
"defs"
"domain"
+ "equivariance"
"extract"
"extract_type"
"finalconsts"
@@ -451,6 +460,7 @@
"method_setup"
"no_syntax"
"no_translations"
+ "nominal_datatype"
"nonterminals"
"notation"
"oracle"
@@ -491,6 +501,8 @@
"instance_proof"
"interpretation"
"lemma"
+ "nominal_inductive"
+ "nominal_primrec"
"pcpodef"
"recdef_tc"
"specification"
--- a/lib/jedit/isabelle.xml Mon Oct 08 18:13:01 2007 +0200
+++ b/lib/jedit/isabelle.xml Mon Oct 08 18:13:03 2007 +0200
@@ -1,6 +1,7 @@
<?xml version="1.0"?>
<!DOCTYPE MODE SYSTEM "xmode.dtd">
-<!-- This file was generated from Pure + HOL + HOLCF + IOA + HOL-Nominal + FOL + ZF -->
+<!-- Generated from Pure + HOL + HOLCF + IOA + HOL-Nominal + FOL + ZF -->
+<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->
<MODE>
<PROPS>
<PROPERTY NAME="commentStart" VALUE="(*"/>
@@ -131,7 +132,6 @@
<OPERATOR>fixpat</OPERATOR>
<OPERATOR>fixrec</OPERATOR>
<KEYWORD4>for</KEYWORD4>
- <KEYWORD4>freshness_context</KEYWORD4>
<OPERATOR>from</OPERATOR>
<LABEL>full_prf</LABEL>
<OPERATOR>fun</OPERATOR>
@@ -168,7 +168,6 @@
<OPERATOR>interpret</OPERATOR>
<OPERATOR>interpretation</OPERATOR>
<KEYWORD4>intros</KEYWORD4>
- <KEYWORD4>invariant</KEYWORD4>
<OPERATOR>invoke</OPERATOR>
<KEYWORD4>is</KEYWORD4>
<OPERATOR>judgment</OPERATOR>