src/HOL/IsaMakefile
changeset 14610 9c2e31e483b2
parent 14603 985eb6708207
child 14626 dfb8d2977263
equal deleted inserted replaced
14609:663e0e435866 14610:9c2e31e483b2
    27   HOL-IOA \
    27   HOL-IOA \
    28   HOL-Induct \
    28   HOL-Induct \
    29   HOL-Isar_examples \
    29   HOL-Isar_examples \
    30   HOL-Lambda \
    30   HOL-Lambda \
    31   HOL-Lattice \
    31   HOL-Lattice \
       
    32   HOL-Matrix \
    32   HOL-MicroJava \
    33   HOL-MicroJava \
    33   HOL-Modelcheck \
    34   HOL-Modelcheck \
    34   HOL-NanoJava \
    35   HOL-NanoJava \
    35   HOL-NumberTheory \
    36   HOL-NumberTheory \
    36   HOL-Prolog \
    37   HOL-Prolog \
   630   SET-Protocol/Purchase.thy\
   631   SET-Protocol/Purchase.thy\
   631   SET-Protocol/document/root.tex 
   632   SET-Protocol/document/root.tex 
   632 	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
   633 	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
   633 
   634 
   634 
   635 
       
   636 ## HOL-Matrix
       
   637 
       
   638 HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
       
   639 
       
   640 $(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ROOT.ML \
       
   641   Matrix/Matrix.thy\
       
   642 	Matrix/LinProg.thy\
       
   643 	Matrix/MatrixGeneral.thy
       
   644 	@$(ISATOOL) usedir $(OUT)/HOL Matrix
       
   645 
       
   646 
   635 
   647 
   636 ## TLA
   648 ## TLA
   637 
   649 
   638 TLA: HOL $(OUT)/TLA
   650 TLA: HOL $(OUT)/TLA
   639 
   651