# HG changeset patch
# User nipkow
# Date 1180109314 -7200
# Node ID 1c84d7294d5b7d5d2341e1364bf36e499df4bef7
# Parent  3d35c78b446fb977c9682611965bc9aa4979511e
Added List_Comprehension

diff -r 3d35c78b446f -r 1c84d7294d5b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 25 06:06:49 2007 +0200
+++ b/src/HOL/IsaMakefile	Fri May 25 18:08:34 2007 +0200
@@ -198,7 +198,7 @@
   Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
   Library/Executable_Real.thy \
   Library/MLString.thy Library/Infinite_Set.thy \
-  Library/FuncSet.thy Library/Library.thy \
+  Library/FuncSet.thy Library/Library.thy Library/List_Comprehension.thy \
   Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy Library/NatPair.thy \
   Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
   Library/Nat_Infinity.thy Library/Word.thy \
diff -r 3d35c78b446f -r 1c84d7294d5b src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri May 25 06:06:49 2007 +0200
+++ b/src/HOL/Library/Library.thy	Fri May 25 18:08:34 2007 +0200
@@ -17,6 +17,7 @@
   FuncSet
   GCD
   Infinite_Set
+  List_Comprehension
   MLString
   Multiset
   NatPair