Added List_Comprehension
authornipkow
Fri May 25 18:08:34 2007 +0200 (2007-05-25)
changeset 231001c84d7294d5b
parent 23099 3d35c78b446f
child 23101 1a05d89feeaf
Added List_Comprehension
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri May 25 06:06:49 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri May 25 18:08:34 2007 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4    Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
     1.5    Library/Executable_Real.thy \
     1.6    Library/MLString.thy Library/Infinite_Set.thy \
     1.7 -  Library/FuncSet.thy Library/Library.thy \
     1.8 +  Library/FuncSet.thy Library/Library.thy Library/List_Comprehension.thy \
     1.9    Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy Library/NatPair.thy \
    1.10    Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
    1.11    Library/Nat_Infinity.thy Library/Word.thy \
     2.1 --- a/src/HOL/Library/Library.thy	Fri May 25 06:06:49 2007 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Fri May 25 18:08:34 2007 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    FuncSet
     2.5    GCD
     2.6    Infinite_Set
     2.7 +  List_Comprehension
     2.8    MLString
     2.9    Multiset
    2.10    NatPair