# HG changeset patch
# User paulson
# Date 861356856 -7200
# Node ID 85c81d524655635276ff67d18c35b5f62843fcc0
# Parent  aa5aeb6467c6e3c56e685007118ceafd342ce5e2
ex/LFilter is a new theory (and dependency)

diff -r aa5aeb6467c6 -r 85c81d524655 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 18 11:47:11 1997 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 18 11:47:36 1997 +0200
@@ -195,8 +195,8 @@
 
 ## Miscellaneous examples
 
-EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
-	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
+EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
+	   Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
diff -r aa5aeb6467c6 -r 85c81d524655 src/HOL/Makefile
--- a/src/HOL/Makefile	Fri Apr 18 11:47:11 1997 +0200
+++ b/src/HOL/Makefile	Fri Apr 18 11:47:36 1997 +0200
@@ -225,8 +225,8 @@
 	fi
 
 ##Miscellaneous examples
-EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
-	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
+EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
+	   Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)