# HG changeset patch
# User wenzelm
# Date 961604068 -7200
# Node ID c7ba07e3bbe8681a7ec309498ed5b36180021803
# Parent  b643f4d7b9e97d621cdfdd2c0ac28c65ddd12de9
fixed deps;

diff -r b643f4d7b9e9 -r c7ba07e3bbe8 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Wed Jun 21 18:09:09 2000 +0200
+++ b/src/HOL/Lambda/Eta.thy	Wed Jun 21 18:14:28 2000 +0200
@@ -6,7 +6,7 @@
 Eta-reduction and relatives.
 *)
 
-Eta = ParRed + Commutation +
+Eta = ParRed +
 consts free :: dB => nat => bool
        decr :: dB => dB
        eta  :: "(dB * dB) set"
diff -r b643f4d7b9e9 -r c7ba07e3bbe8 src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Wed Jun 21 18:09:09 2000 +0200
+++ b/src/HOL/Lambda/InductTermi.thy	Wed Jun 21 18:14:28 2000 +0200
@@ -9,7 +9,7 @@
 Also rediscovered by Matthes and Joachimski.
 *)
 
-InductTermi = Acc + ListBeta +
+InductTermi = ListBeta +
 
 consts IT :: dB set
 inductive IT
diff -r b643f4d7b9e9 -r c7ba07e3bbe8 src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Wed Jun 21 18:09:09 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.thy	Wed Jun 21 18:14:28 2000 +0200
@@ -6,7 +6,7 @@
 Application of a term to a list of terms
 *)
 
-ListApplication = Lambda + List +
+ListApplication = Lambda +
 
 syntax "$$" :: dB => dB list => dB (infixl 150)
 translations "t $$ ts" == "foldl op$ t ts"
diff -r b643f4d7b9e9 -r c7ba07e3bbe8 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Wed Jun 21 18:09:09 2000 +0200
+++ b/src/HOL/Lambda/ListOrder.thy	Wed Jun 21 18:14:28 2000 +0200
@@ -6,7 +6,7 @@
 Lifting an order to lists of elements, relating exactly one element
 *)
 
-ListOrder = List + Acc +
+ListOrder = Acc +
 
 constdefs
  step1 :: "('a * 'a)set => ('a list * 'a list)set"