--- a/IntEx.thy	Tue Oct 27 11:03:38 2009 +0100
+++ b/IntEx.thy	Tue Oct 27 11:27:53 2009 +0100
@@ -144,13 +144,6 @@
   lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t
 *}
 
-lemma plus_sym_pre:
-  shows "intrel (my_plus a b) (my_plus b a)"
-  apply (cases a)
-  apply (cases b)
-  apply (simp)
-  done
-
 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}
 
 lemma plus_assoc_pre:

--- a/QuotMain.thy	Tue Oct 27 11:03:38 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 11:27:53 2009 +0100
@@ -15,9 +15,13 @@
 begin
 
 definition
+  ABS::"'a \<Rightarrow> 'b"
+where
   "ABS x \<equiv> Abs (R x)"
 
 definition
+  REP::"'b \<Rightarrow> 'a"
+where
   "REP a = Eps (Rep a)"
 
 lemma lem9:
@@ -100,19 +104,8 @@
   assumes ac: "R a c"
   and     bd: "R b d"
   shows "R a b = R c d"
-proof
-  assume "R a b"
-  then have "R b a" using R_sym by blast
-  then have "R b c" using ac R_trans by blast
-  then have "R c b" using R_sym by blast
-  then show "R c d" using bd R_trans by blast
-next
-  assume "R c d"
-  then have "R a d" using ac R_trans by blast
-  then have "R d a" using R_sym by blast
-  then have "R b a" using bd R_trans by blast
-  then show "R a b" using R_sym by blast
-qed
+using ac bd
+by (blast intro: R_trans R_sym)
 
 lemma REPS_same:
   shows "R (REP a) (REP b) \<equiv> (a = b)"

--- a/isar-keywords-prove.el	Tue Oct 27 11:03:38 2009 +0100
+++ b/isar-keywords-prove.el	Tue Oct 27 11:27:53 2009 +0100
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + Pure + Pure-ProofGeneral + HOL-Nominal-test.
+;; Generated from HOL + Pure + Pure-ProofGeneral + HOL-Nominal-test + HOL-Nominal.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -28,6 +28,7 @@
     "apply_end"
     "arities"
     "assume"
+    "atom_decl"
     "atp_info"
     "atp_kill"
     "atp_messages"
@@ -84,6 +85,7 @@
     "done"
     "enable_pr"
     "end"
+    "equivariance"
     "exit"
     "export_code"
     "extract"
@@ -128,6 +130,10 @@
     "no_notation"
     "no_syntax"
     "no_translations"
+    "nominal_datatype"
+    "nominal_inductive"
+    "nominal_inductive2"
+    "nominal_primrec"
     "nonterminals"
     "normal_form"
     "notation"
@@ -251,6 +257,7 @@
     "and"
     "assumes"
     "attach"
+    "avoids"
     "begin"
     "binder"
     "congs"
@@ -397,6 +404,7 @@
   '("ML"
     "abbreviation"
     "arities"
+    "atom_decl"
     "attribute_setup"
     "axclass"
     "axiomatization"
@@ -429,6 +437,7 @@
     "defer_recdef"
     "definition"
     "defs"
+    "equivariance"
     "extract"
     "extract_type"
     "finalconsts"
@@ -447,6 +456,7 @@
     "no_notation"
     "no_syntax"
     "no_translations"
+    "nominal_datatype"
     "nonterminals"
     "notation"
     "oracle"
@@ -487,6 +497,9 @@
     "instance"
     "interpretation"
     "lemma"
+    "nominal_inductive"
+    "nominal_inductive2"
+    "nominal_primrec"
     "prove"
     "quotient"
     "recdef_tc"