--- 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"
--- 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
--- 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"
--- 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"