# HG changeset patch
# User kuncar
# Date 1343738635 -7200
# Node ID 77c416ef06fa3e48d3661427d2d25360fe4d6da3
# Parent  9b71daba4ec7fc4d9c6fdd870bcc8923f1c40114
Remove Lift_RBT.thy, it's in HOL/Library/RBT.thy now

diff -r 9b71daba4ec7 -r 77c416ef06fa src/HOL/IsaMakefile
--- 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
 
diff -r 9b71daba4ec7 -r 77c416ef06fa src/HOL/Quotient_Examples/Lift_RBT.thy
--- 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
diff -r 9b71daba4ec7 -r 77c416ef06fa src/HOL/Quotient_Examples/ROOT.ML
--- 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"];
 
diff -r 9b71daba4ec7 -r 77c416ef06fa src/HOL/ROOT
--- 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