src/HOL/IsaMakefile
changeset 32667 09546e654222
parent 32662 2faf1148c062
child 32674 b629fbcc5313
     1.1 --- a/src/HOL/IsaMakefile	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  default: HOL
     1.6  generate: HOL-Generate-HOL HOL-Generate-HOLLight
     1.7 -images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4 HOL-MicroJava
     1.8 +images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
     1.9  
    1.10  #Note: keep targets sorted (except for HOL-Library and HOL-ex)
    1.11  test: \
    1.12 @@ -909,7 +909,7 @@
    1.13    ex/Sudoku.thy ex/Tarski.thy \
    1.14    ex/Termination.thy ex/Transfer_Ex.thy ex/Unification.thy ex/document/root.bib		\
    1.15    ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
    1.16 -  ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
    1.17 +  ex/Predicate_Compile.thy Tools/Predicate_Compile/predicate_compile_core.ML ex/Predicate_Compile_ex.thy
    1.18  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
    1.19  
    1.20