Nominal/Nominal2_FSet.thy
changeset 2550 551c5a8b6b2c
parent 2542 1f5c8e85c41f
child 2559 add799cf0817
--- a/Nominal/Nominal2_FSet.thy	Tue Oct 19 15:08:24 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Thu Oct 28 14:03:46 2010 +0900
@@ -1,7 +1,7 @@
 theory Nominal2_FSet
 imports "../Nominal-General/Nominal2_Base"
         "../Nominal-General/Nominal2_Eqvt" 
-        FSet 
+        "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet"
 begin
 
 lemma permute_fset_rsp[quot_respect]: