--- a/src/HOL/IsaMakefile Tue Jul 31 13:55:39 2012 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 31 14:43:55 2012 +0200
@@ -1528,7 +1528,7 @@
Quotient_Examples/FSet.thy \
Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
Quotient_Examples/Lift_FSet.thy \
- Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \
+ Quotient_Examples/Lift_Set.thy \
Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
--- a/src/HOL/Quotient_Examples/Lift_RBT.thy Tue Jul 31 13:55:39 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title: HOL/Quotient_Examples/Lift_RBT.thy
- Author: Lukas Bulwahn and Ondrej Kuncar
-*)
-
-header {* Lifting operations of RBT trees *}
-
-theory Lift_RBT
-imports Main "~~/src/HOL/Library/RBT_Impl"
-begin
-
-(* Moved to ~~/HOL/Library/RBT" *)
-
-end
\ No newline at end of file
--- a/src/HOL/Quotient_Examples/ROOT.ML Tue Jul 31 13:55:39 2012 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML Tue Jul 31 14:43:55 2012 +0200
@@ -5,5 +5,5 @@
*)
use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Lift_FSet",
- "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat", "Lift_DList"];
+ "Lift_Set", "Lift_Fun", "Quotient_Rat", "Lift_DList"];
--- a/src/HOL/ROOT Tue Jul 31 13:55:39 2012 +0200
+++ b/src/HOL/ROOT Tue Jul 31 14:43:55 2012 +0200
@@ -758,7 +758,6 @@
Quotient_Message
Lift_FSet
Lift_Set
- Lift_RBT
Lift_Fun
Quotient_Rat
Lift_DList