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]: