src/HOL/IsaMakefile
changeset 7917 5e5b9813cce7
parent 7799 4c69318e6a6d
child 7926 9c20924de52c
equal deleted inserted replaced
7916:3cb310f40a3a 7917:5e5b9813cce7
    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/HahnBanachExtLemmas.thy	\
   105   Real/HahnBanach/HahnBanach_lemmas.thy		\
   105   Real/HahnBanach/HahnBanachSupLemmas.thy	\
   106   Real/HahnBanach/LinearSpace.thy Real/HahnBanach/Linearform.thy \
   106   Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
   107   Real/HahnBanach/NormedSpace.thy Real/HahnBanach/ROOT.ML \
   107   Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
   108   Real/HahnBanach/Subspace.thy Real/HahnBanach/Zorn_Lemma.thy \
   108   Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
   109   Real/HahnBanach/document/notation.tex		\
   109   Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/notation.tex \
   110   Real/HahnBanach/document/root.tex
   110   Real/HahnBanach/document/root.tex
   111 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
   111 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
   112 
   112 
   113 
   113 
   114 ## HOL-Subst
   114 ## HOL-Subst