# HG changeset patch
# User kuncar
# Date 1323438378 -3600
# Node ID e832acb88f43b33fe278322b90e6c9ad54fea7e4
# Parent  7fa9410c746a5ead7db72f1352c3ed00ef5d1f67
added dependencies

diff -r 7fa9410c746a -r e832acb88f43 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Dec 09 14:22:05 2011 +0100
+++ b/src/HOL/IsaMakefile	Fri Dec 09 14:46:18 2011 +0100
@@ -1508,7 +1508,8 @@
   Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \
   Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \
   Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
-  Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy
+  Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \
+  Quotient_Examples/Lift_Fun.thy 
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
 
 
diff -r 7fa9410c746a -r e832acb88f43 src/HOL/Quotient_Examples/ROOT.ML
--- a/src/HOL/Quotient_Examples/ROOT.ML	Fri Dec 09 14:22:05 2011 +0100
+++ b/src/HOL/Quotient_Examples/ROOT.ML	Fri Dec 09 14:46:18 2011 +0100
@@ -5,5 +5,5 @@
 *)
 
 use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset",
-  "List_Quotient_Cset", "Lift_Set", "Lift_RBT"];
+  "List_Quotient_Cset", "Lift_Set", "Lift_RBT", "Lift_Fun"];