src/HOL/IsaMakefile
changeset 30101 5c6efec476ae
parent 30096 c5497842ee35
parent 29748 2ff24d87fad1
child 30160 5f7b17941730
equal deleted inserted replaced
30100:e1c714d33c5c 30101:5c6efec476ae
    11 #Note: keep targets sorted (except for HOL-Library and HOL-ex)
    11 #Note: keep targets sorted (except for HOL-Library and HOL-ex)
    12 test: \
    12 test: \
    13   HOL-Library \
    13   HOL-Library \
    14   HOL-ex \
    14   HOL-ex \
    15   HOL-Auth \
    15   HOL-Auth \
    16   HOL-AxClasses \
       
    17   HOL-Bali \
    16   HOL-Bali \
    18   HOL-Decision_Procs \
    17   HOL-Decision_Procs \
    19   HOL-Extraction \
    18   HOL-Extraction \
    20   HOL-HahnBanach \
    19   HOL-HahnBanach \
    21   HOL-Hoare \
    20   HOL-Hoare \
   794 $(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML	\
   793 $(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML	\
   795   IOA/Solve.thy
   794   IOA/Solve.thy
   796 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
   795 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
   797 
   796 
   798 
   797 
   799 ## HOL-AxClasses
       
   800 
       
   801 HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
       
   802 
       
   803 $(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy			\
       
   804   AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
       
   805 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL AxClasses
       
   806 
       
   807 
       
   808 ## HOL-Lattice
   798 ## HOL-Lattice
   809 
   799 
   810 HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
   800 HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
   811 
   801 
   812 $(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy			\
   802 $(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy			\
  1066 
  1056 
  1067 
  1057 
  1068 ## clean
  1058 ## clean
  1069 
  1059 
  1070 clean:
  1060 clean:
  1071 	@rm -f  $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL $(OUT)/HOL-Nominal $(OUT)/TLA \
  1061 	@rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL		\
  1072 		$(LOG)/HOL.gz $(LOG)/TLA.gz \
  1062 		$(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz		\
  1073 		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
  1063 		$(LOG)/TLA.gz $(LOG)/HOL-Isar_examples.gz		\
  1074 		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
  1064 		$(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz			\
  1075 		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
  1065 		$(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz			\
  1076 		$(LOG)/HOL-HoareParallel.gz \
  1066 		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz			\
  1077 		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
  1067 		$(LOG)/HOL-HoareParallel.gz $(LOG)/HOL-Lex.gz		\
  1078 		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
  1068 		$(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz		\
  1079 		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
  1069 		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz		\
  1080                 $(LOG)/HOL-Bali.gz \
  1070 		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz			\
  1081 		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
  1071 		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz		\
  1082                 $(LOG)/HOL-Nominal-Examples.gz \
  1072 		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz	\
  1083 		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
  1073 		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix			\
  1084 		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
  1074 		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz	\
  1085 		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
  1075 		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz			\
  1086                 $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
  1076 		$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz		\
  1087 		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz \
  1077 		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
  1088                 $(OUT)/HOL-Word $(LOG)/HOL-Word.gz $(LOG)/HOL-Word-Examples.gz \
  1078 		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
  1089                 $(OUT)/HOL-NSA $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz
  1079 		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz