src/HOL/IsaMakefile
changeset 7799 4c69318e6a6d
parent 7760 43f8d28dbc6e
child 7917 5e5b9813cce7
equal deleted inserted replaced
7798:42e94b618f34 7799:4c69318e6a6d
    96 
    96 
    97 ## HOL-Real-HahnBanach
    97 ## HOL-Real-HahnBanach
    98 
    98 
    99 HOL-Real-HahnBanach: HOL-Real $(LOG)/HOL-Real-HahnBanach.gz
    99 HOL-Real-HahnBanach: HOL-Real $(LOG)/HOL-Real-HahnBanach.gz
   100 
   100 
   101 $(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy	\
   101 $(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy \
   102   Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
   102   Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
   103   Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
   103   Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
   104   Real/HahnBanach/HahnBanach_h0_lemmas.thy				\
   104   Real/HahnBanach/HahnBanach_h0_lemmas.thy	\
   105   Real/HahnBanach/HahnBanach_lemmas.thy					\
   105   Real/HahnBanach/HahnBanach_lemmas.thy		\
   106   Real/HahnBanach/LinearSpace.thy Real/HahnBanach/Linearform.thy	\
   106   Real/HahnBanach/LinearSpace.thy Real/HahnBanach/Linearform.thy \
   107   Real/HahnBanach/NormedSpace.thy Real/HahnBanach/ROOT.ML		\
   107   Real/HahnBanach/NormedSpace.thy Real/HahnBanach/ROOT.ML \
   108   Real/HahnBanach/Subspace.thy Real/HahnBanach/Zorn_Lemma.thy
   108   Real/HahnBanach/Subspace.thy Real/HahnBanach/Zorn_Lemma.thy \
       
   109   Real/HahnBanach/document/notation.tex		\
       
   110   Real/HahnBanach/document/root.tex
   109 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
   111 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
   110 
   112 
   111 
   113 
   112 ## HOL-Subst
   114 ## HOL-Subst
   113 
   115 
   370   Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
   372   Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
   371   Isar_examples/ExprCompiler.thy Isar_examples/Group.thy \
   373   Isar_examples/ExprCompiler.thy Isar_examples/Group.thy \
   372   Isar_examples/KnasterTarski.thy Isar_examples/MultisetOrder.thy \
   374   Isar_examples/KnasterTarski.thy Isar_examples/MultisetOrder.thy \
   373   Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \
   375   Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \
   374   Isar_examples/Summation.thy Isar_examples/ROOT.ML \
   376   Isar_examples/Summation.thy Isar_examples/ROOT.ML \
   375   Isar_examples/W_correct.thy
   377   Isar_examples/W_correct.thy Isar_examples/document/root.tex \
       
   378   Isar_examples/document/style.tex
   376 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
   379 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
   377 
   380 
   378 
   381 
   379 ## TLA
   382 ## TLA
   380 
   383