# HG changeset patch
# User wenzelm
# Date 971905288 -7200
# Node ID ef384b242d0982de256e6378f025432b58087b07
# Parent  9cc18073294593840e1fe4b5fee8b0084821aa2c
use Accessible_Part from HOL/Library;

diff -r 9cc180732945 -r ef384b242d09 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Wed Oct 18 23:40:58 2000 +0200
+++ b/src/HOL/Lambda/ListOrder.thy	Wed Oct 18 23:41:28 2000 +0200
@@ -6,7 +6,7 @@
 
 header {* Lifting an order to lists of elements *}
 
-theory ListOrder = Acc:
+theory ListOrder = Accessible_Part:
 
 text {*
   Lifting an order to lists of elements, relating exactly one
diff -r 9cc180732945 -r ef384b242d09 src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Wed Oct 18 23:40:58 2000 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Wed Oct 18 23:41:28 2000 +0200
@@ -5,5 +5,5 @@
 *)
 
 time_use_thy "Eta";
-with_path "../Induct" time_use_thy "Acc";
+time_use_thy "Accessible_Part";
 time_use_thy "Type";