ex/LFilter is a new theory (and dependency)
authorpaulson
Fri Apr 18 11:47:36 1997 +0200 (1997-04-18)
changeset 298285c81d524655
parent 2981 aa5aeb6467c6
child 2983 f914a1663b2a
ex/LFilter is a new theory (and dependency)
src/HOL/IsaMakefile
src/HOL/Makefile
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 18 11:47:11 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 18 11:47:36 1997 +0200
     1.3 @@ -195,8 +195,8 @@
     1.4  
     1.5  ## Miscellaneous examples
     1.6  
     1.7 -EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
     1.8 -	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
     1.9 +EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
    1.10 +	   Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
    1.11  
    1.12  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
    1.13  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
     2.1 --- a/src/HOL/Makefile	Fri Apr 18 11:47:11 1997 +0200
     2.2 +++ b/src/HOL/Makefile	Fri Apr 18 11:47:36 1997 +0200
     2.3 @@ -225,8 +225,8 @@
     2.4  	fi
     2.5  
     2.6  ##Miscellaneous examples
     2.7 -EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
     2.8 -	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
     2.9 +EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
    2.10 +	   Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
    2.11  
    2.12  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
    2.13  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)