ex/LFilter is a new theory (and dependency)
authorpaulson
Fri, 18 Apr 1997 11:47:36 +0200
changeset 2982 85c81d524655
parent 2981 aa5aeb6467c6
child 2983 f914a1663b2a
ex/LFilter is a new theory (and dependency)
src/HOL/IsaMakefile
src/HOL/Makefile
--- 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)
--- 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)