use Accessible_Part from HOL/Library;
authorwenzelm
Wed, 18 Oct 2000 23:41:28 +0200
changeset 10264 ef384b242d09
parent 10263 9cc180732945
child 10265 4e004b548049
use Accessible_Part from HOL/Library;
src/HOL/Lambda/ListOrder.thy
src/HOL/Lambda/ROOT.ML
--- 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
--- 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";