853 $(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML \ |
848 $(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML \ |
854 Docs/document/root.tex |
849 Docs/document/root.tex |
855 @$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs |
850 @$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs |
856 |
851 |
857 |
852 |
|
853 ## HOL-Proofs |
|
854 |
|
855 HOL-Proofs: Pure $(OUT)/HOL-Proofs |
|
856 |
|
857 $(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES) |
|
858 @$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs |
|
859 |
|
860 |
|
861 ## HOL-Proofs-ex |
|
862 |
|
863 HOL-Proofs-ex: HOL-Proofs $(LOG)/HOL-Proofs-ex.gz |
|
864 |
|
865 $(LOG)/HOL-Proofs-ex.gz: $(OUT)/HOL-Proofs \ |
|
866 Proofs/ex/ROOT.ML Proofs/ex/Hilbert_Classical.thy |
|
867 @cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs ex |
|
868 |
|
869 |
|
870 ## HOL-Proofs-Extraction |
|
871 |
|
872 HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz |
|
873 |
|
874 $(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \ |
|
875 Library/Efficient_Nat.thy Proofs/Extraction/Euclid.thy \ |
|
876 Proofs/Extraction/Greatest_Common_Divisor.thy \ |
|
877 Proofs/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.thy \ |
|
878 Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML \ |
|
879 Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy \ |
|
880 Proofs/Extraction/document/root.tex \ |
|
881 Proofs/Extraction/document/root.bib |
|
882 @cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction |
|
883 |
|
884 |
858 ## HOL-Proofs-Lambda |
885 ## HOL-Proofs-Lambda |
859 |
886 |
860 HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz |
887 HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz |
861 |
888 |
862 $(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs Lambda/Commutation.thy \ |
889 $(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs \ |
863 Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \ |
890 Proofs/Lambda/Commutation.thy Proofs/Lambda/Eta.thy \ |
864 Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \ |
891 Proofs/Lambda/InductTermi.thy Proofs/Lambda/Lambda.thy \ |
865 Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy \ |
892 Proofs/Lambda/ListApplication.thy Proofs/Lambda/ListBeta.thy \ |
866 Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy \ |
893 Proofs/Lambda/ListOrder.thy Proofs/Lambda/NormalForm.thy \ |
867 Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex |
894 Proofs/Lambda/ParRed.thy Proofs/Lambda/Standardization.thy \ |
868 @$(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda |
895 Proofs/Lambda/StrongNorm.thy Proofs/Lambda/Type.thy \ |
|
896 Proofs/Lambda/WeakNorm.thy Proofs/Lambda/ROOT.ML \ |
|
897 Proofs/Lambda/document/root.bib Proofs/Lambda/document/root.tex |
|
898 @cd Proofs; $(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda |
869 |
899 |
870 |
900 |
871 ## HOL-Prolog |
901 ## HOL-Prolog |
872 |
902 |
873 HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz |
903 HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz |
938 Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy \ |
968 Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy \ |
939 Bali/document/root.tex |
969 Bali/document/root.tex |
940 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali |
970 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali |
941 |
971 |
942 |
972 |
943 ## HOL-Proofs-Extraction |
|
944 |
|
945 HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz |
|
946 |
|
947 $(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \ |
|
948 Library/Efficient_Nat.thy Extraction/Euclid.thy \ |
|
949 Extraction/Greatest_Common_Divisor.thy Extraction/Higman.thy \ |
|
950 Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML \ |
|
951 Extraction/Util.thy Extraction/Warshall.thy \ |
|
952 Extraction/document/root.tex Extraction/document/root.bib |
|
953 @$(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction |
|
954 |
|
955 |
|
956 ## HOL-IOA |
973 ## HOL-IOA |
957 |
974 |
958 HOL-IOA: HOL $(LOG)/HOL-IOA.gz |
975 HOL-IOA: HOL $(LOG)/HOL-IOA.gz |
959 |
976 |
960 $(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML \ |
977 $(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML \ |
975 ## HOL-ex |
992 ## HOL-ex |
976 |
993 |
977 HOL-ex: HOL $(LOG)/HOL-ex.gz |
994 HOL-ex: HOL $(LOG)/HOL-ex.gz |
978 |
995 |
979 $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \ |
996 $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \ |
980 Number_Theory/Primes.thy \ |
997 Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \ |
981 ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \ |
998 ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \ |
982 ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \ |
999 ex/BinEx.thy ex/Binary.thy ex/CTL.thy ex/Chinese.thy \ |
983 ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \ |
1000 ex/Classical.thy ex/CodegenSML_Test.thy ex/Coherent.thy \ |
984 ex/CodegenSML_Test.thy ex/Coherent.thy ex/Dedekind_Real.thy \ |
1001 ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \ |
985 ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \ |
1002 ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \ |
986 ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \ |
1003 ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ |
987 ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \ |
1004 ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ |
988 ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \ |
|
989 ex/Induction_Schema.thy ex/InductiveInvariant.thy \ |
1005 ex/Induction_Schema.thy ex/InductiveInvariant.thy \ |
990 ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ |
1006 ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ |
991 ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ |
1007 ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \ |
992 ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \ |
1008 ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ |
993 ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \ |
1009 ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ |
994 ex/PresburgerEx.thy ex/Primrec.thy \ |
1010 ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \ |
995 ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \ |
|
996 ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ |
1011 ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ |
997 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
1012 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
998 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \ |
1013 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \ |
999 ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \ |
1014 ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \ |
1000 ex/Unification.thy ex/While_Combinator_Example.thy ex/document/root.bib \ |
1015 ex/Unification.thy ex/While_Combinator_Example.thy \ |
1001 ex/document/root.tex \ |
1016 ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \ |
1002 ex/set.thy ex/svc_funcs.ML ex/svc_test.thy |
1017 ex/svc_test.thy |
1003 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
1018 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
1004 |
1019 |
1005 |
1020 |
1006 ## HOL-Isar_Examples |
1021 ## HOL-Isar_Examples |
1007 |
1022 |
1135 Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy \ |
1150 Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy \ |
1136 Probability/Lebesgue_Measure.thy \ |
1151 Probability/Lebesgue_Measure.thy \ |
1137 Library/Nat_Bijection.thy Library/Countable.thy |
1152 Library/Nat_Bijection.thy Library/Countable.thy |
1138 @cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability |
1153 @cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability |
1139 |
1154 |
|
1155 |
1140 ## HOL-Nominal |
1156 ## HOL-Nominal |
1141 |
1157 |
1142 HOL-Nominal: HOL $(OUT)/HOL-Nominal |
1158 HOL-Nominal: HOL $(OUT)/HOL-Nominal |
1143 |
1159 |
1144 $(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \ |
1160 $(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \ |
1158 |
1174 |
1159 ## HOL-Nominal-Examples |
1175 ## HOL-Nominal-Examples |
1160 |
1176 |
1161 HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz |
1177 HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz |
1162 |
1178 |
1163 $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \ |
1179 $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \ |
1164 Nominal/Examples/Nominal_Examples.thy \ |
1180 Nominal/Examples/Nominal_Examples.thy \ |
1165 Nominal/Examples/CK_Machine.thy \ |
1181 Nominal/Examples/CK_Machine.thy \ |
1166 Nominal/Examples/CR.thy \ |
1182 Nominal/Examples/CR.thy \ |
1167 Nominal/Examples/CR_Takahashi.thy \ |
1183 Nominal/Examples/CR_Takahashi.thy \ |
1168 Nominal/Examples/Class1.thy \ |
1184 Nominal/Examples/Class1.thy \ |
1350 $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz \ |
1366 $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz \ |
1351 $(LOG)/HOL-Number_Theory.gz \ |
1367 $(LOG)/HOL-Number_Theory.gz \ |
1352 $(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz \ |
1368 $(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz \ |
1353 $(LOG)/HOL-Predicate_Compile_Examples.gz \ |
1369 $(LOG)/HOL-Predicate_Compile_Examples.gz \ |
1354 $(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz \ |
1370 $(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz \ |
1355 $(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-Extraction.gz \ |
1371 $(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz \ |
|
1372 $(LOG)/HOL-Proofs-Extraction.gz \ |
1356 $(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \ |
1373 $(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \ |
1357 $(LOG)/HOL-Word-SMT_Examples.gz \ |
1374 $(LOG)/HOL-Word-SMT_Examples.gz \ |
1358 $(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \ |
1375 $(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \ |
1359 $(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \ |
1376 $(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \ |
1360 $(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \ |
1377 $(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \ |