Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IsaMakefile
changeset 33024 60a098883d81
parent 33010 39f73a59e855
child 33026 8f35633c4922
equal deleted inserted replaced
33023:207c21697a48 33024:60a098883d81 
   835 
   835 
   836 ## HOL-Bali
 
   836 ## HOL-Bali
 
   837 
   837 
   838 HOL-Bali: HOL $(LOG)/HOL-Bali.gz
 
   838 HOL-Bali: HOL $(LOG)/HOL-Bali.gz
 
   839 
   839 
   840 $(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy Bali/AxExample.thy	\
 
   840 $(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy		\
 
   841   Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy	\
 
   841   Bali/AxExample.thy Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy	\
 
   842   Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy	\
 
   842   Bali/Conform.thy Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy	\
 
   843   Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy		\
 
   843   Bali/Evaln.thy Bali/Example.thy Bali/Name.thy Bali/ROOT.ML		\
 
   844   Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy		\
 
   844   Bali/State.thy Bali/Table.thy Bali/Term.thy Bali/Trans.thy		\
 
   845   Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
 
   845   Bali/Type.thy Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy	\
 
   846   Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy	\
 
   846   Bali/WellForm.thy Bali/DefiniteAssignment.thy				\
 
   847   Bali/WellType.thy Bali/document/root.tex
 
   847   Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy			\
 
       
   848   Bali/document/root.tex
 
   848 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
 
   849 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
 
   849 
   850 
   850 
   851 
   851 ## HOL-Extraction
 
   852 ## HOL-Extraction
 
   852 
   853 
   883 ## HOL-ex
 
   884 ## HOL-ex
 
   884 
   885 
   885 HOL-ex: HOL $(LOG)/HOL-ex.gz
 
   886 HOL-ex: HOL $(LOG)/HOL-ex.gz
 
   886 
   887 
   887 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy		\
 
   888 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy		\
 
   888   Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
 
   889   Number_Theory/Primes.thy						\
 
   889   ex/Arith_Examples.thy				\
 
   890   Tools/Predicate_Compile/predicate_compile_core.ML			\
 
       
   891   ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy		\
 
   890   ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy		\
 
   892   ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy		\
 
   891   ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
 
   893   ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
 
   892   ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy				\
 
   894   ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy		\
 
   893   ex/Codegenerator_Pretty.thy ex/Codegenerator_Test.thy \
 
   895   ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy		\
 
   894   ex/Codegenerator_Pretty_Test.thy ex/Coherent.thy				\
 
   896   ex/Codegenerator_Test.thy ex/Coherent.thy ex/Commutative_RingEx.thy	\
 
   895   ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy		\
 
   897   ex/Commutative_Ring_Complete.thy ex/Efficient_Nat_examples.thy	\
 
   896   ex/Efficient_Nat_examples.thy		\
 
   898   ex/Eval_Examples.thy ex/Fundefs.thy ex/Groebner_Examples.thy		\
 
   897   ex/Eval_Examples.thy	ex/Fundefs.thy			\
 
   899   ex/Guess.thy ex/HarmonicSeries.thy ex/Hebrew.thy			\
 
   898   ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
 
   900   ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy			\
 
   899   ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
 
   901   ex/Hilbert_Classical.thy ex/Induction_Scheme.thy			\
 
   900   ex/Hilbert_Classical.thy			\
 
   902   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
 
   901   ex/Induction_Scheme.thy ex/InductiveInvariant.thy			\
 
   903   ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy	\
 
   902   ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
 
   904   ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
 
   903   ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy		\
 
   905   ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
 
   904   ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
 
   906   ex/Predicate_Compile.thy ex/Predicate_Compile_ex.thy			\
 
   905   ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
 
   907   ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
 
   906   ex/Quickcheck_Examples.thy ex/ROOT.ML	\
 
   908   ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
 
   907   ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
 
       
   908   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
 
   909   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
 
   909   ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
 
   910   ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\
 
   910   ex/Sudoku.thy ex/Tarski.thy \
 
   911   ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy			\
 
   911   ex/Termination.thy ex/Transfer_Ex.thy ex/Unification.thy ex/document/root.bib		\
 
   912   ex/Unification.thy ex/document/root.bib ex/document/root.tex		\
 
   912   ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
 
   913   ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
 
   913   ex/Predicate_Compile.thy Tools/Predicate_Compile/predicate_compile_core.ML ex/Predicate_Compile_ex.thy
 
       
   914 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
 
   914 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
 
   915 
   915 
   916 
   916 
   917 ## HOL-Isar_examples
 
   917 ## HOL-Isar_examples
 
   918 
   918 
   985 
   985 
   986 ## TLA-Buffer
 
   986 ## TLA-Buffer
 
   987 
   987 
   988 TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
 
   988 TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
 
   989 
   989 
   990 $(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy TLA/Buffer/DBuffer.thy
 
   990 $(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy	\
 
       
   991   TLA/Buffer/DBuffer.thy
 
   991 	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
 
   992 	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
 
   992 
   993 
   993 
   994 
   994 ## TLA-Memory
 
   995 ## TLA-Memory
 
   995 
   996 
  1054 
  1055 
  1055 ## HOL-Word
 
  1056 ## HOL-Word
 
  1056 
  1057 
  1057 HOL-Word: HOL $(OUT)/HOL-Word
 
  1058 HOL-Word: HOL $(OUT)/HOL-Word
 
  1058 
  1059 
  1059 $(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML	\
 
  1060 $(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy	\
 
  1060   Library/Boolean_Algebra.thy			\
 
       
  1061   Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy		\
 
  1061   Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy		\
 
  1062   Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy		\
 
  1062   Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy		\
 
  1063   Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy	\
 
  1063   Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy	\
 
  1064   Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy		\
 
  1064   Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy		\
 
  1065   Word/WordGenLib.thy Word/Word.thy Word/document/root.tex		\
 
  1065   Word/WordGenLib.thy Word/Word.thy Word/document/root.tex		\
 
  1090 
  1090 
  1091 ## HOL-NSA
 
  1091 ## HOL-NSA
 
  1092 
  1092 
  1093 HOL-NSA: HOL $(OUT)/HOL-NSA
 
  1093 HOL-NSA: HOL $(OUT)/HOL-NSA
 
  1094 
  1094 
  1095 $(OUT)/HOL-NSA: $(OUT)/HOL \
 
  1095 $(OUT)/HOL-NSA: $(OUT)/HOL NSA/CLim.thy NSA/CStar.thy NSA/NSCA.thy	\
 
  1096   NSA/CLim.thy \
 
  1096   NSA/NSComplex.thy NSA/HDeriv.thy NSA/HLim.thy NSA/HLog.thy		\
 
  1097   NSA/CStar.thy \
 
  1097   NSA/HSEQ.thy NSA/HSeries.thy NSA/HTranscendental.thy			\
 
  1098   NSA/NSCA.thy \
 
  1098   NSA/Hypercomplex.thy NSA/HyperDef.thy NSA/HyperNat.thy		\
 
  1099   NSA/NSComplex.thy \
 
  1099   NSA/Hyperreal.thy NSA/Filter.thy NSA/NatStar.thy NSA/NSA.thy		\
 
  1100   NSA/HDeriv.thy \
 
  1100   NSA/StarDef.thy NSA/Star.thy NSA/transfer.ML				\
 
  1101   NSA/HLim.thy \
 
  1101   Library/Infinite_Set.thy Library/Zorn.thy NSA/ROOT.ML
 
  1102   NSA/HLog.thy \
 
       
  1103   NSA/HSEQ.thy \
 
       
  1104   NSA/HSeries.thy \
 
       
  1105   NSA/HTranscendental.thy \
 
       
  1106   NSA/Hypercomplex.thy \
 
       
  1107   NSA/HyperDef.thy \
 
       
  1108   NSA/HyperNat.thy \
 
       
  1109   NSA/Hyperreal.thy \
 
       
  1110   NSA/Filter.thy \
 
       
  1111   NSA/NatStar.thy \
 
       
  1112   NSA/NSA.thy \
 
       
  1113   NSA/StarDef.thy \
 
       
  1114   NSA/Star.thy \
 
       
  1115   NSA/transfer.ML \
 
       
  1116   Library/Infinite_Set.thy \
 
       
  1117   Library/Zorn.thy \
 
       
  1118   NSA/ROOT.ML
 
       
  1119 	@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
 
  1102 	@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
 
  1120 
  1103 
  1121 
  1104 
  1122 ## HOL-NSA-Examples
 
  1105 ## HOL-NSA-Examples
 
  1123 
  1106 
  1130 
  1113 
  1131 ## HOL-Mirabelle
 
  1114 ## HOL-Mirabelle
 
  1132 
  1115 
  1133 HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
 
  1116 HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
 
  1134 
  1117 
  1135 $(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy \
 
  1118 $(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy	\
 
  1136   Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML Mirabelle/ROOT.ML \
 
  1119   Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML			\
 
  1137   Mirabelle/Tools/mirabelle_arith.ML \
 
  1120   Mirabelle/ROOT.ML Mirabelle/Tools/mirabelle_arith.ML			\
 
  1138   Mirabelle/Tools/mirabelle_metis.ML \
 
  1121   Mirabelle/Tools/mirabelle_metis.ML					\
 
  1139   Mirabelle/Tools/mirabelle_quickcheck.ML \
 
  1122   Mirabelle/Tools/mirabelle_quickcheck.ML				\
 
  1140   Mirabelle/Tools/mirabelle_refute.ML \
 
  1123   Mirabelle/Tools/mirabelle_refute.ML					\
 
  1141   Mirabelle/Tools/mirabelle_sledgehammer.ML
 
  1124   Mirabelle/Tools/mirabelle_sledgehammer.ML
 
  1142 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
 
  1125 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
 
  1143 
  1126 
  1144 
  1127 
  1145 ## HOL-SMT
 
  1128 ## HOL-SMT
 
  1146 
  1129 
  1147 HOL-SMT: HOL-Word $(LOG)/HOL-SMT.gz
 
  1130 HOL-SMT: HOL-Word $(OUT)/HOL-SMT
 
  1148 
  1131 
  1149 $(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy SMT/SMT.thy \
 
  1132 $(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy		\
 
  1150   SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
 
  1133   SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML	\
 
  1151   SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \
 
  1134   SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML			\
 
  1152   SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \
 
  1135   SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML			\
 
  1153   SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \
 
  1136   SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML			\
 
  1154   SMT/Tools/z3_proof_terms.ML SMT/Tools/z3_proof_rules.ML \
 
  1137   SMT/Tools/z3_proof_terms.ML SMT/Tools/z3_proof_rules.ML		\
 
  1155   SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML \
 
  1138   SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML				\
 
  1156   SMT/Tools/z3_solver.ML
 
  1139   SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
 
  1157 	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
 
  1140 	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
 
  1158 
  1141 
  1159 
  1142 
  1160 ## HOL-SMT-Examples
 
  1143 ## HOL-SMT-Examples
 
  1161 
  1144 
  1162 HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz
 
  1145 HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz
 
  1163 
  1146 
  1164 $(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML	\
 
  1147 $(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML		\
 
  1165   SMT/Examples/SMT_Examples.thy \
 
  1148   SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01	\
 
  1166   SMT/Examples/cert/z3_arith_quant_01 \
 
  1149   SMT/Examples/cert/z3_arith_quant_01.proof				\
 
  1167   SMT/Examples/cert/z3_arith_quant_01.proof \
 
  1150   SMT/Examples/cert/z3_arith_quant_02					\
 
  1168   SMT/Examples/cert/z3_arith_quant_02 \
 
  1151   SMT/Examples/cert/z3_arith_quant_02.proof				\
 
  1169   SMT/Examples/cert/z3_arith_quant_02.proof \
 
  1152   SMT/Examples/cert/z3_arith_quant_03					\
 
  1170   SMT/Examples/cert/z3_arith_quant_03 \
 
  1153   SMT/Examples/cert/z3_arith_quant_03.proof				\
 
  1171   SMT/Examples/cert/z3_arith_quant_03.proof \
 
  1154   SMT/Examples/cert/z3_arith_quant_04					\
 
  1172   SMT/Examples/cert/z3_arith_quant_04 \
 
  1155   SMT/Examples/cert/z3_arith_quant_04.proof				\
 
  1173   SMT/Examples/cert/z3_arith_quant_04.proof \
 
  1156   SMT/Examples/cert/z3_arith_quant_05					\
 
  1174   SMT/Examples/cert/z3_arith_quant_05 \
 
  1157   SMT/Examples/cert/z3_arith_quant_05.proof				\
 
  1175   SMT/Examples/cert/z3_arith_quant_05.proof \
 
  1158   SMT/Examples/cert/z3_arith_quant_06					\
 
  1176   SMT/Examples/cert/z3_arith_quant_06 \
 
  1159   SMT/Examples/cert/z3_arith_quant_06.proof				\
 
  1177   SMT/Examples/cert/z3_arith_quant_06.proof \
 
  1160   SMT/Examples/cert/z3_arith_quant_07					\
 
  1178   SMT/Examples/cert/z3_arith_quant_07 \
 
  1161   SMT/Examples/cert/z3_arith_quant_07.proof				\
 
  1179   SMT/Examples/cert/z3_arith_quant_07.proof \
 
  1162   SMT/Examples/cert/z3_arith_quant_08					\
 
  1180   SMT/Examples/cert/z3_arith_quant_08 \
 
  1163   SMT/Examples/cert/z3_arith_quant_08.proof				\
 
  1181   SMT/Examples/cert/z3_arith_quant_08.proof \
 
  1164   SMT/Examples/cert/z3_arith_quant_09					\
 
  1182   SMT/Examples/cert/z3_arith_quant_09 \
 
  1165   SMT/Examples/cert/z3_arith_quant_09.proof				\
 
  1183   SMT/Examples/cert/z3_arith_quant_09.proof \
 
  1166   SMT/Examples/cert/z3_arith_quant_10					\
 
  1184   SMT/Examples/cert/z3_arith_quant_10 \
 
  1167   SMT/Examples/cert/z3_arith_quant_10.proof				\
 
  1185   SMT/Examples/cert/z3_arith_quant_10.proof \
 
  1168   SMT/Examples/cert/z3_arith_quant_11					\
 
  1186   SMT/Examples/cert/z3_arith_quant_11 \
 
  1169   SMT/Examples/cert/z3_arith_quant_11.proof				\
 
  1187   SMT/Examples/cert/z3_arith_quant_11.proof \
 
  1170   SMT/Examples/cert/z3_arith_quant_12					\
 
  1188   SMT/Examples/cert/z3_arith_quant_12 \
 
  1171   SMT/Examples/cert/z3_arith_quant_12.proof				\
 
  1189   SMT/Examples/cert/z3_arith_quant_12.proof \
 
  1172   SMT/Examples/cert/z3_arith_quant_13					\
 
  1190   SMT/Examples/cert/z3_arith_quant_13 \
 
  1173   SMT/Examples/cert/z3_arith_quant_13.proof				\
 
  1191   SMT/Examples/cert/z3_arith_quant_13.proof \
 
  1174   SMT/Examples/cert/z3_arith_quant_14					\
 
  1192   SMT/Examples/cert/z3_arith_quant_14 \
 
  1175   SMT/Examples/cert/z3_arith_quant_14.proof				\
 
  1193   SMT/Examples/cert/z3_arith_quant_14.proof \
 
  1176   SMT/Examples/cert/z3_arith_quant_15					\
 
  1194   SMT/Examples/cert/z3_arith_quant_15 \
 
  1177   SMT/Examples/cert/z3_arith_quant_15.proof				\
 
  1195   SMT/Examples/cert/z3_arith_quant_15.proof \
 
  1178   SMT/Examples/cert/z3_arith_quant_16					\
 
  1196   SMT/Examples/cert/z3_arith_quant_16 \
 
  1179   SMT/Examples/cert/z3_arith_quant_16.proof				\
 
  1197   SMT/Examples/cert/z3_arith_quant_16.proof \
 
  1180   SMT/Examples/cert/z3_arith_quant_17					\
 
  1198   SMT/Examples/cert/z3_arith_quant_17 \
 
  1181   SMT/Examples/cert/z3_arith_quant_17.proof				\
 
  1199   SMT/Examples/cert/z3_arith_quant_17.proof \
 
  1182   SMT/Examples/cert/z3_arith_quant_18					\
 
  1200   SMT/Examples/cert/z3_arith_quant_18 \
 
  1183   SMT/Examples/cert/z3_arith_quant_18.proof SMT/Examples/cert/z3_bv_01	\
 
  1201   SMT/Examples/cert/z3_arith_quant_18.proof \
 
  1184   SMT/Examples/cert/z3_bv_01.proof SMT/Examples/cert/z3_bv_02		\
 
  1202   SMT/Examples/cert/z3_bv_01 \
 
  1185   SMT/Examples/cert/z3_bv_02.proof SMT/Examples/cert/z3_bv_arith_01	\
 
  1203   SMT/Examples/cert/z3_bv_01.proof \
 
  1186   SMT/Examples/cert/z3_bv_arith_01.proof				\
 
  1204   SMT/Examples/cert/z3_bv_02 \
 
  1187   SMT/Examples/cert/z3_bv_arith_02					\
 
  1205   SMT/Examples/cert/z3_bv_02.proof \
 
  1188   SMT/Examples/cert/z3_bv_arith_02.proof				\
 
  1206   SMT/Examples/cert/z3_bv_arith_01 \
 
  1189   SMT/Examples/cert/z3_bv_arith_03					\
 
  1207   SMT/Examples/cert/z3_bv_arith_01.proof \
 
  1190   SMT/Examples/cert/z3_bv_arith_03.proof				\
 
  1208   SMT/Examples/cert/z3_bv_arith_02 \
 
  1191   SMT/Examples/cert/z3_bv_arith_04					\
 
  1209   SMT/Examples/cert/z3_bv_arith_02.proof \
 
  1192   SMT/Examples/cert/z3_bv_arith_04.proof				\
 
  1210   SMT/Examples/cert/z3_bv_arith_03 \
 
  1193   SMT/Examples/cert/z3_bv_arith_05					\
 
  1211   SMT/Examples/cert/z3_bv_arith_03.proof \
 
  1194   SMT/Examples/cert/z3_bv_arith_05.proof				\
 
  1212   SMT/Examples/cert/z3_bv_arith_04 \
 
  1195   SMT/Examples/cert/z3_bv_arith_06					\
 
  1213   SMT/Examples/cert/z3_bv_arith_04.proof \
 
  1196   SMT/Examples/cert/z3_bv_arith_06.proof				\
 
  1214   SMT/Examples/cert/z3_bv_arith_05 \
 
  1197   SMT/Examples/cert/z3_bv_arith_07					\
 
  1215   SMT/Examples/cert/z3_bv_arith_05.proof \
 
  1198   SMT/Examples/cert/z3_bv_arith_07.proof				\
 
  1216   SMT/Examples/cert/z3_bv_arith_06 \
 
  1199   SMT/Examples/cert/z3_bv_arith_08					\
 
  1217   SMT/Examples/cert/z3_bv_arith_06.proof \
 
  1200   SMT/Examples/cert/z3_bv_arith_08.proof				\
 
  1218   SMT/Examples/cert/z3_bv_arith_07 \
 
  1201   SMT/Examples/cert/z3_bv_arith_09					\
 
  1219   SMT/Examples/cert/z3_bv_arith_07.proof \
 
  1202   SMT/Examples/cert/z3_bv_arith_09.proof				\
 
  1220   SMT/Examples/cert/z3_bv_arith_08 \
 
  1203   SMT/Examples/cert/z3_bv_arith_10					\
 
  1221   SMT/Examples/cert/z3_bv_arith_08.proof \
 
  1204   SMT/Examples/cert/z3_bv_arith_10.proof				\
 
  1222   SMT/Examples/cert/z3_bv_arith_09 \
 
  1205   SMT/Examples/cert/z3_bv_bit_01 SMT/Examples/cert/z3_bv_bit_01.proof	\
 
  1223   SMT/Examples/cert/z3_bv_arith_09.proof \
 
  1206   SMT/Examples/cert/z3_bv_bit_02 SMT/Examples/cert/z3_bv_bit_02.proof	\
 
  1224   SMT/Examples/cert/z3_bv_arith_10 \
 
  1207   SMT/Examples/cert/z3_bv_bit_03 SMT/Examples/cert/z3_bv_bit_03.proof	\
 
  1225   SMT/Examples/cert/z3_bv_arith_10.proof \
 
  1208   SMT/Examples/cert/z3_bv_bit_04 SMT/Examples/cert/z3_bv_bit_04.proof	\
 
  1226   SMT/Examples/cert/z3_bv_bit_01 \
 
  1209   SMT/Examples/cert/z3_bv_bit_05 SMT/Examples/cert/z3_bv_bit_05.proof	\
 
  1227   SMT/Examples/cert/z3_bv_bit_01.proof \
 
  1210   SMT/Examples/cert/z3_bv_bit_06 SMT/Examples/cert/z3_bv_bit_06.proof	\
 
  1228   SMT/Examples/cert/z3_bv_bit_02 \
 
  1211   SMT/Examples/cert/z3_bv_bit_07 SMT/Examples/cert/z3_bv_bit_07.proof	\
 
  1229   SMT/Examples/cert/z3_bv_bit_02.proof \
 
  1212   SMT/Examples/cert/z3_bv_bit_08 SMT/Examples/cert/z3_bv_bit_08.proof	\
 
  1230   SMT/Examples/cert/z3_bv_bit_03 \
 
  1213   SMT/Examples/cert/z3_bv_bit_09 SMT/Examples/cert/z3_bv_bit_09.proof	\
 
  1231   SMT/Examples/cert/z3_bv_bit_03.proof \
 
  1214   SMT/Examples/cert/z3_bv_bit_10 SMT/Examples/cert/z3_bv_bit_10.proof	\
 
  1232   SMT/Examples/cert/z3_bv_bit_04 \
 
  1215   SMT/Examples/cert/z3_bv_bit_11 SMT/Examples/cert/z3_bv_bit_11.proof	\
 
  1233   SMT/Examples/cert/z3_bv_bit_04.proof \
 
  1216   SMT/Examples/cert/z3_bv_bit_12 SMT/Examples/cert/z3_bv_bit_12.proof	\
 
  1234   SMT/Examples/cert/z3_bv_bit_05 \
 
  1217   SMT/Examples/cert/z3_bv_bit_13 SMT/Examples/cert/z3_bv_bit_13.proof	\
 
  1235   SMT/Examples/cert/z3_bv_bit_05.proof \
 
  1218   SMT/Examples/cert/z3_bv_bit_14 SMT/Examples/cert/z3_bv_bit_14.proof	\
 
  1236   SMT/Examples/cert/z3_bv_bit_06 \
 
  1219   SMT/Examples/cert/z3_bv_bit_15 SMT/Examples/cert/z3_bv_bit_15.proof	\
 
  1237   SMT/Examples/cert/z3_bv_bit_06.proof \
 
  1220   SMT/Examples/cert/z3_fol_01 SMT/Examples/cert/z3_fol_01.proof		\
 
  1238   SMT/Examples/cert/z3_bv_bit_07 \
 
  1221   SMT/Examples/cert/z3_fol_02 SMT/Examples/cert/z3_fol_02.proof		\
 
  1239   SMT/Examples/cert/z3_bv_bit_07.proof \
 
  1222   SMT/Examples/cert/z3_fol_03 SMT/Examples/cert/z3_fol_03.proof		\
 
  1240   SMT/Examples/cert/z3_bv_bit_08 \
 
  1223   SMT/Examples/cert/z3_fol_04 SMT/Examples/cert/z3_fol_04.proof		\
 
  1241   SMT/Examples/cert/z3_bv_bit_08.proof \
 
  1224   SMT/Examples/cert/z3_hol_01 SMT/Examples/cert/z3_hol_01.proof		\
 
  1242   SMT/Examples/cert/z3_bv_bit_09 \
 
  1225   SMT/Examples/cert/z3_hol_02 SMT/Examples/cert/z3_hol_02.proof		\
 
  1243   SMT/Examples/cert/z3_bv_bit_09.proof \
 
  1226   SMT/Examples/cert/z3_hol_03 SMT/Examples/cert/z3_hol_03.proof		\
 
  1244   SMT/Examples/cert/z3_bv_bit_10 \
 
  1227   SMT/Examples/cert/z3_hol_04 SMT/Examples/cert/z3_hol_04.proof		\
 
  1245   SMT/Examples/cert/z3_bv_bit_10.proof \
 
  1228   SMT/Examples/cert/z3_hol_05 SMT/Examples/cert/z3_hol_05.proof		\
 
  1246   SMT/Examples/cert/z3_bv_bit_11 \
 
  1229   SMT/Examples/cert/z3_hol_06 SMT/Examples/cert/z3_hol_06.proof		\
 
  1247   SMT/Examples/cert/z3_bv_bit_11.proof \
 
  1230   SMT/Examples/cert/z3_hol_07 SMT/Examples/cert/z3_hol_07.proof		\
 
  1248   SMT/Examples/cert/z3_bv_bit_12 \
 
  1231   SMT/Examples/cert/z3_hol_08 SMT/Examples/cert/z3_hol_08.proof		\
 
  1249   SMT/Examples/cert/z3_bv_bit_12.proof \
 
  1232   SMT/Examples/cert/z3_linarith_01					\
 
  1250   SMT/Examples/cert/z3_bv_bit_13 \
 
  1233   SMT/Examples/cert/z3_linarith_01.proof				\
 
  1251   SMT/Examples/cert/z3_bv_bit_13.proof \
 
  1234   SMT/Examples/cert/z3_linarith_02					\
 
  1252   SMT/Examples/cert/z3_bv_bit_14 \
 
  1235   SMT/Examples/cert/z3_linarith_02.proof				\
 
  1253   SMT/Examples/cert/z3_bv_bit_14.proof \
 
  1236   SMT/Examples/cert/z3_linarith_03					\
 
  1254   SMT/Examples/cert/z3_bv_bit_15 \
 
  1237   SMT/Examples/cert/z3_linarith_03.proof				\
 
  1255   SMT/Examples/cert/z3_bv_bit_15.proof \
 
  1238   SMT/Examples/cert/z3_linarith_04					\
 
  1256   SMT/Examples/cert/z3_fol_01 \
 
  1239   SMT/Examples/cert/z3_linarith_04.proof				\
 
  1257   SMT/Examples/cert/z3_fol_01.proof \
 
  1240   SMT/Examples/cert/z3_linarith_05					\
 
  1258   SMT/Examples/cert/z3_fol_02 \
 
  1241   SMT/Examples/cert/z3_linarith_05.proof				\
 
  1259   SMT/Examples/cert/z3_fol_02.proof \
 
  1242   SMT/Examples/cert/z3_linarith_06					\
 
  1260   SMT/Examples/cert/z3_fol_03 \
 
  1243   SMT/Examples/cert/z3_linarith_06.proof				\
 
  1261   SMT/Examples/cert/z3_fol_03.proof \
 
  1244   SMT/Examples/cert/z3_linarith_07					\
 
  1262   SMT/Examples/cert/z3_fol_04 \
 
  1245   SMT/Examples/cert/z3_linarith_07.proof				\
 
  1263   SMT/Examples/cert/z3_fol_04.proof \
 
  1246   SMT/Examples/cert/z3_linarith_08					\
 
  1264   SMT/Examples/cert/z3_hol_01 \
 
  1247   SMT/Examples/cert/z3_linarith_08.proof				\
 
  1265   SMT/Examples/cert/z3_hol_01.proof \
 
  1248   SMT/Examples/cert/z3_linarith_09					\
 
  1266   SMT/Examples/cert/z3_hol_02 \
 
  1249   SMT/Examples/cert/z3_linarith_09.proof				\
 
  1267   SMT/Examples/cert/z3_hol_02.proof \
 
  1250   SMT/Examples/cert/z3_linarith_10					\
 
  1268   SMT/Examples/cert/z3_hol_03 \
 
  1251   SMT/Examples/cert/z3_linarith_10.proof				\
 
  1269   SMT/Examples/cert/z3_hol_03.proof \
 
  1252   SMT/Examples/cert/z3_linarith_11					\
 
  1270   SMT/Examples/cert/z3_hol_04 \
 
  1253   SMT/Examples/cert/z3_linarith_11.proof				\
 
  1271   SMT/Examples/cert/z3_hol_04.proof \
 
  1254   SMT/Examples/cert/z3_linarith_12					\
 
  1272   SMT/Examples/cert/z3_hol_05 \
 
  1255   SMT/Examples/cert/z3_linarith_12.proof				\
 
  1273   SMT/Examples/cert/z3_hol_05.proof \
 
  1256   SMT/Examples/cert/z3_linarith_13					\
 
  1274   SMT/Examples/cert/z3_hol_06 \
 
  1257   SMT/Examples/cert/z3_linarith_13.proof				\
 
  1275   SMT/Examples/cert/z3_hol_06.proof \
 
  1258   SMT/Examples/cert/z3_linarith_14					\
 
  1276   SMT/Examples/cert/z3_hol_07 \
 
  1259   SMT/Examples/cert/z3_linarith_14.proof				\
 
  1277   SMT/Examples/cert/z3_hol_07.proof \
 
  1260   SMT/Examples/cert/z3_linarith_15					\
 
  1278   SMT/Examples/cert/z3_hol_08 \
 
  1261   SMT/Examples/cert/z3_linarith_15.proof				\
 
  1279   SMT/Examples/cert/z3_hol_08.proof \
 
  1262   SMT/Examples/cert/z3_linarith_16					\
 
  1280   SMT/Examples/cert/z3_linarith_01 \
 
  1263   SMT/Examples/cert/z3_linarith_16.proof SMT/Examples/cert/z3_mono_01	\
 
  1281   SMT/Examples/cert/z3_linarith_01.proof \
 
  1264   SMT/Examples/cert/z3_mono_01.proof SMT/Examples/cert/z3_mono_02	\
 
  1282   SMT/Examples/cert/z3_linarith_02 \
 
  1265   SMT/Examples/cert/z3_mono_02.proof SMT/Examples/cert/z3_nat_arith_01	\
 
  1283   SMT/Examples/cert/z3_linarith_02.proof \
 
  1266   SMT/Examples/cert/z3_nat_arith_01.proof				\
 
  1284   SMT/Examples/cert/z3_linarith_03 \
 
  1267   SMT/Examples/cert/z3_nat_arith_02					\
 
  1285   SMT/Examples/cert/z3_linarith_03.proof \
 
  1268   SMT/Examples/cert/z3_nat_arith_02.proof				\
 
  1286   SMT/Examples/cert/z3_linarith_04 \
 
  1269   SMT/Examples/cert/z3_nat_arith_03					\
 
  1287   SMT/Examples/cert/z3_linarith_04.proof \
 
  1270   SMT/Examples/cert/z3_nat_arith_03.proof				\
 
  1288   SMT/Examples/cert/z3_linarith_05 \
 
  1271   SMT/Examples/cert/z3_nat_arith_04					\
 
  1289   SMT/Examples/cert/z3_linarith_05.proof \
 
  1272   SMT/Examples/cert/z3_nat_arith_04.proof				\
 
  1290   SMT/Examples/cert/z3_linarith_06 \
 
  1273   SMT/Examples/cert/z3_nat_arith_05					\
 
  1291   SMT/Examples/cert/z3_linarith_06.proof \
 
  1274   SMT/Examples/cert/z3_nat_arith_05.proof				\
 
  1292   SMT/Examples/cert/z3_linarith_07 \
 
  1275   SMT/Examples/cert/z3_nat_arith_06					\
 
  1293   SMT/Examples/cert/z3_linarith_07.proof \
 
  1276   SMT/Examples/cert/z3_nat_arith_06.proof				\
 
  1294   SMT/Examples/cert/z3_linarith_08 \
 
  1277   SMT/Examples/cert/z3_nat_arith_07					\
 
  1295   SMT/Examples/cert/z3_linarith_08.proof \
 
  1278   SMT/Examples/cert/z3_nat_arith_07.proof				\
 
  1296   SMT/Examples/cert/z3_linarith_09 \
 
  1279   SMT/Examples/cert/z3_nlarith_01					\
 
  1297   SMT/Examples/cert/z3_linarith_09.proof \
 
  1280   SMT/Examples/cert/z3_nlarith_01.proof					\
 
  1298   SMT/Examples/cert/z3_linarith_10 \
 
  1281   SMT/Examples/cert/z3_nlarith_02					\
 
  1299   SMT/Examples/cert/z3_linarith_10.proof \
 
  1282   SMT/Examples/cert/z3_nlarith_02.proof					\
 
  1300   SMT/Examples/cert/z3_linarith_11 \
 
  1283   SMT/Examples/cert/z3_nlarith_03					\
 
  1301   SMT/Examples/cert/z3_linarith_11.proof \
 
  1284   SMT/Examples/cert/z3_nlarith_03.proof					\
 
  1302   SMT/Examples/cert/z3_linarith_12 \
 
  1285   SMT/Examples/cert/z3_nlarith_04					\
 
  1303   SMT/Examples/cert/z3_linarith_12.proof \
 
  1286   SMT/Examples/cert/z3_nlarith_04.proof SMT/Examples/cert/z3_pair_01	\
 
  1304   SMT/Examples/cert/z3_linarith_13 \
 
  1287   SMT/Examples/cert/z3_pair_01.proof SMT/Examples/cert/z3_pair_02	\
 
  1305   SMT/Examples/cert/z3_linarith_13.proof \
 
  1288   SMT/Examples/cert/z3_pair_02.proof SMT/Examples/cert/z3_prop_01	\
 
  1306   SMT/Examples/cert/z3_linarith_14 \
 
  1289   SMT/Examples/cert/z3_prop_01.proof SMT/Examples/cert/z3_prop_02	\
 
  1307   SMT/Examples/cert/z3_linarith_14.proof \
 
  1290   SMT/Examples/cert/z3_prop_02.proof SMT/Examples/cert/z3_prop_03	\
 
  1308   SMT/Examples/cert/z3_linarith_15 \
 
  1291   SMT/Examples/cert/z3_prop_03.proof SMT/Examples/cert/z3_prop_04	\
 
  1309   SMT/Examples/cert/z3_linarith_15.proof \
 
  1292   SMT/Examples/cert/z3_prop_04.proof SMT/Examples/cert/z3_prop_05	\
 
  1310   SMT/Examples/cert/z3_linarith_16 \
 
  1293   SMT/Examples/cert/z3_prop_05.proof SMT/Examples/cert/z3_prop_06	\
 
  1311   SMT/Examples/cert/z3_linarith_16.proof \
 
  1294   SMT/Examples/cert/z3_prop_06.proof SMT/Examples/cert/z3_prop_07	\
 
  1312   SMT/Examples/cert/z3_mono_01 \
 
  1295   SMT/Examples/cert/z3_prop_07.proof SMT/Examples/cert/z3_prop_08	\
 
  1313   SMT/Examples/cert/z3_mono_01.proof \
 
  1296   SMT/Examples/cert/z3_prop_08.proof SMT/Examples/cert/z3_prop_09	\
 
  1314   SMT/Examples/cert/z3_mono_02 \
 
  1297   SMT/Examples/cert/z3_prop_09.proof SMT/Examples/cert/z3_prop_10	\
 
  1315   SMT/Examples/cert/z3_mono_02.proof \
 
       
  1316   SMT/Examples/cert/z3_nat_arith_01 \
 
       
  1317   SMT/Examples/cert/z3_nat_arith_01.proof \
 
       
  1318   SMT/Examples/cert/z3_nat_arith_02 \
 
       
  1319   SMT/Examples/cert/z3_nat_arith_02.proof \
 
       
  1320   SMT/Examples/cert/z3_nat_arith_03 \
 
       
  1321   SMT/Examples/cert/z3_nat_arith_03.proof \
 
       
  1322   SMT/Examples/cert/z3_nat_arith_04 \
 
       
  1323   SMT/Examples/cert/z3_nat_arith_04.proof \
 
       
  1324   SMT/Examples/cert/z3_nat_arith_05 \
 
       
  1325   SMT/Examples/cert/z3_nat_arith_05.proof \
 
       
  1326   SMT/Examples/cert/z3_nat_arith_06 \
 
       
  1327   SMT/Examples/cert/z3_nat_arith_06.proof \
 
       
  1328   SMT/Examples/cert/z3_nat_arith_07 \
 
       
  1329   SMT/Examples/cert/z3_nat_arith_07.proof \
 
       
  1330   SMT/Examples/cert/z3_nlarith_01 \
 
       
  1331   SMT/Examples/cert/z3_nlarith_01.proof \
 
       
  1332   SMT/Examples/cert/z3_nlarith_02 \
 
       
  1333   SMT/Examples/cert/z3_nlarith_02.proof \
 
       
  1334   SMT/Examples/cert/z3_nlarith_03 \
 
       
  1335   SMT/Examples/cert/z3_nlarith_03.proof \
 
       
  1336   SMT/Examples/cert/z3_nlarith_04 \
 
       
  1337   SMT/Examples/cert/z3_nlarith_04.proof \
 
       
  1338   SMT/Examples/cert/z3_pair_01 \
 
       
  1339   SMT/Examples/cert/z3_pair_01.proof \
 
       
  1340   SMT/Examples/cert/z3_pair_02 \
 
       
  1341   SMT/Examples/cert/z3_pair_02.proof \
 
       
  1342   SMT/Examples/cert/z3_prop_01 \
 
       
  1343   SMT/Examples/cert/z3_prop_01.proof \
 
       
  1344   SMT/Examples/cert/z3_prop_02 \
 
       
  1345   SMT/Examples/cert/z3_prop_02.proof \
 
       
  1346   SMT/Examples/cert/z3_prop_03 \
 
       
  1347   SMT/Examples/cert/z3_prop_03.proof \
 
       
  1348   SMT/Examples/cert/z3_prop_04 \
 
       
  1349   SMT/Examples/cert/z3_prop_04.proof \
 
       
  1350   SMT/Examples/cert/z3_prop_05 \
 
       
  1351   SMT/Examples/cert/z3_prop_05.proof \
 
       
  1352   SMT/Examples/cert/z3_prop_06 \
 
       
  1353   SMT/Examples/cert/z3_prop_06.proof \
 
       
  1354   SMT/Examples/cert/z3_prop_07 \
 
       
  1355   SMT/Examples/cert/z3_prop_07.proof \
 
       
  1356   SMT/Examples/cert/z3_prop_08 \
 
       
  1357   SMT/Examples/cert/z3_prop_08.proof \
 
       
  1358   SMT/Examples/cert/z3_prop_09 \
 
       
  1359   SMT/Examples/cert/z3_prop_09.proof \
 
       
  1360   SMT/Examples/cert/z3_prop_10 \
 
       
  1361   SMT/Examples/cert/z3_prop_10.proof
 
  1298   SMT/Examples/cert/z3_prop_10.proof
 
  1362 	@cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples
 
  1299 	@cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples
 
  1363 
  1300 
  1364 
  1301 
  1365 ## clean
 
  1302 ## clean
isabelle