# HG changeset patch
# User haftmann
# Date 1314533774 -7200
# Node ID 1fc97d6083fd8a15cfa7121bed05f3033269eeb8
# Parent  bf8331161ad99043d9c59abd2a780fee4bd174b5
tuned

diff -r bf8331161ad9 -r 1fc97d6083fd src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sun Aug 28 13:13:27 2011 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Sun Aug 28 14:16:14 2011 +0200
@@ -3608,7 +3608,7 @@
 
 (************************************************************)
 (* various tactics for analysing permutations, supports etc *)
-use "nominal_permeq.ML";
+use "nominal_permeq.ML"
 
 method_setup perm_simp =
   {* NominalPermeq.perm_simp_meth *}
@@ -3652,7 +3652,7 @@
 
 (*****************************************************************)
 (* tactics for generating fresh names and simplifying fresh_funs *)
-use "nominal_fresh_fun.ML";
+use "nominal_fresh_fun.ML"
 
 method_setup generate_fresh = 
   {* setup_generate_fresh *} 
@@ -3681,7 +3681,7 @@
 
 (*****************************************)
 (* setup for induction principles method *)
-use "nominal_induct.ML";
+use "nominal_induct.ML"
 method_setup nominal_induct =
   {* NominalInduct.nominal_induct_method *}
   {* nominal induction *}