fixed deps;
authorwenzelm
Wed Jun 21 18:14:28 2000 +0200 (2000-06-21)
changeset 9102c7ba07e3bbe8
parent 9101 b643f4d7b9e9
child 9103 ef56f093259d
fixed deps;
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListOrder.thy
     1.1 --- a/src/HOL/Lambda/Eta.thy	Wed Jun 21 18:09:09 2000 +0200
     1.2 +++ b/src/HOL/Lambda/Eta.thy	Wed Jun 21 18:14:28 2000 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  Eta-reduction and relatives.
     1.5  *)
     1.6  
     1.7 -Eta = ParRed + Commutation +
     1.8 +Eta = ParRed +
     1.9  consts free :: dB => nat => bool
    1.10         decr :: dB => dB
    1.11         eta  :: "(dB * dB) set"
     2.1 --- a/src/HOL/Lambda/InductTermi.thy	Wed Jun 21 18:09:09 2000 +0200
     2.2 +++ b/src/HOL/Lambda/InductTermi.thy	Wed Jun 21 18:14:28 2000 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  Also rediscovered by Matthes and Joachimski.
     2.5  *)
     2.6  
     2.7 -InductTermi = Acc + ListBeta +
     2.8 +InductTermi = ListBeta +
     2.9  
    2.10  consts IT :: dB set
    2.11  inductive IT
     3.1 --- a/src/HOL/Lambda/ListApplication.thy	Wed Jun 21 18:09:09 2000 +0200
     3.2 +++ b/src/HOL/Lambda/ListApplication.thy	Wed Jun 21 18:14:28 2000 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  Application of a term to a list of terms
     3.5  *)
     3.6  
     3.7 -ListApplication = Lambda + List +
     3.8 +ListApplication = Lambda +
     3.9  
    3.10  syntax "$$" :: dB => dB list => dB (infixl 150)
    3.11  translations "t $$ ts" == "foldl op$ t ts"
     4.1 --- a/src/HOL/Lambda/ListOrder.thy	Wed Jun 21 18:09:09 2000 +0200
     4.2 +++ b/src/HOL/Lambda/ListOrder.thy	Wed Jun 21 18:14:28 2000 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  Lifting an order to lists of elements, relating exactly one element
     4.5  *)
     4.6  
     4.7 -ListOrder = List + Acc +
     4.8 +ListOrder = Acc +
     4.9  
    4.10  constdefs
    4.11   step1 :: "('a * 'a)set => ('a list * 'a list)set"