--- a/src/HOL/IsaMakefile Tue Oct 20 19:28:01 2009 +0200
+++ b/src/HOL/IsaMakefile Tue Oct 20 19:29:24 2009 +0200
@@ -837,14 +837,15 @@
HOL-Bali: HOL $(LOG)/HOL-Bali.gz
-$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy Bali/AxExample.thy \
- Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy \
- Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy \
- Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy \
- Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy \
- Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy \
- Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy \
- Bali/WellType.thy Bali/document/root.tex
+$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy \
+ Bali/AxExample.thy Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy \
+ Bali/Conform.thy Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy \
+ Bali/Evaln.thy Bali/Example.thy Bali/Name.thy Bali/ROOT.ML \
+ Bali/State.thy Bali/Table.thy Bali/Term.thy Bali/Trans.thy \
+ Bali/Type.thy Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy \
+ Bali/WellForm.thy Bali/DefiniteAssignment.thy \
+ Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy \
+ Bali/document/root.tex
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
@@ -885,32 +886,31 @@
HOL-ex: HOL $(LOG)/HOL-ex.gz
$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
- Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
- ex/Arith_Examples.thy \
+ Number_Theory/Primes.thy \
+ Tools/Predicate_Compile/predicate_compile_core.ML \
+ ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \
ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \
- ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy \
- ex/Codegenerator_Pretty.thy ex/Codegenerator_Test.thy \
- ex/Codegenerator_Pretty_Test.thy ex/Coherent.thy \
- ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy \
- ex/Efficient_Nat_examples.thy \
- ex/Eval_Examples.thy ex/Fundefs.thy \
- ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
- ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
- ex/Hilbert_Classical.thy \
- ex/Induction_Scheme.thy ex/InductiveInvariant.thy \
- ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \
- ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \
- ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
- ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
- ex/Quickcheck_Examples.thy ex/ROOT.ML \
- ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
+ ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy \
+ ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy \
+ ex/Codegenerator_Test.thy ex/Coherent.thy ex/Commutative_RingEx.thy \
+ ex/Commutative_Ring_Complete.thy ex/Efficient_Nat_examples.thy \
+ ex/Eval_Examples.thy ex/Fundefs.thy ex/Groebner_Examples.thy \
+ ex/Guess.thy ex/HarmonicSeries.thy ex/Hebrew.thy \
+ ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
+ ex/Hilbert_Classical.thy ex/Induction_Scheme.thy \
+ ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
+ ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
+ ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
+ ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \
+ ex/Predicate_Compile.thy ex/Predicate_Compile_ex.thy \
+ ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \
+ ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
- ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
- ex/Sudoku.thy ex/Tarski.thy \
- ex/Termination.thy ex/Transfer_Ex.thy ex/Unification.thy ex/document/root.bib \
- ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
- ex/Predicate_Compile.thy Tools/Predicate_Compile/predicate_compile_core.ML ex/Predicate_Compile_ex.thy
+ ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \
+ ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \
+ ex/Unification.thy ex/document/root.bib ex/document/root.tex \
+ ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
@@ -987,7 +987,8 @@
TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
-$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy TLA/Buffer/DBuffer.thy
+$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy \
+ TLA/Buffer/DBuffer.thy
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
@@ -1056,8 +1057,7 @@
HOL-Word: HOL $(OUT)/HOL-Word
-$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML \
- Library/Boolean_Algebra.thy \
+$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy \
Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy \
Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy \
Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy \
@@ -1092,30 +1092,13 @@
HOL-NSA: HOL $(OUT)/HOL-NSA
-$(OUT)/HOL-NSA: $(OUT)/HOL \
- NSA/CLim.thy \
- NSA/CStar.thy \
- NSA/NSCA.thy \
- NSA/NSComplex.thy \
- NSA/HDeriv.thy \
- NSA/HLim.thy \
- NSA/HLog.thy \
- NSA/HSEQ.thy \
- NSA/HSeries.thy \
- NSA/HTranscendental.thy \
- NSA/Hypercomplex.thy \
- NSA/HyperDef.thy \
- NSA/HyperNat.thy \
- NSA/Hyperreal.thy \
- NSA/Filter.thy \
- NSA/NatStar.thy \
- NSA/NSA.thy \
- NSA/StarDef.thy \
- NSA/Star.thy \
- NSA/transfer.ML \
- Library/Infinite_Set.thy \
- Library/Zorn.thy \
- NSA/ROOT.ML
+$(OUT)/HOL-NSA: $(OUT)/HOL NSA/CLim.thy NSA/CStar.thy NSA/NSCA.thy \
+ NSA/NSComplex.thy NSA/HDeriv.thy NSA/HLim.thy NSA/HLog.thy \
+ NSA/HSEQ.thy NSA/HSeries.thy NSA/HTranscendental.thy \
+ NSA/Hypercomplex.thy NSA/HyperDef.thy NSA/HyperNat.thy \
+ NSA/Hyperreal.thy NSA/Filter.thy NSA/NatStar.thy NSA/NSA.thy \
+ NSA/StarDef.thy NSA/Star.thy NSA/transfer.ML \
+ Library/Infinite_Set.thy Library/Zorn.thy NSA/ROOT.ML
@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
@@ -1132,28 +1115,28 @@
HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
-$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy \
- Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML Mirabelle/ROOT.ML \
- Mirabelle/Tools/mirabelle_arith.ML \
- Mirabelle/Tools/mirabelle_metis.ML \
- Mirabelle/Tools/mirabelle_quickcheck.ML \
- Mirabelle/Tools/mirabelle_refute.ML \
+$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy \
+ Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML \
+ Mirabelle/ROOT.ML Mirabelle/Tools/mirabelle_arith.ML \
+ Mirabelle/Tools/mirabelle_metis.ML \
+ Mirabelle/Tools/mirabelle_quickcheck.ML \
+ Mirabelle/Tools/mirabelle_refute.ML \
Mirabelle/Tools/mirabelle_sledgehammer.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
## HOL-SMT
-HOL-SMT: HOL-Word $(LOG)/HOL-SMT.gz
+HOL-SMT: HOL-Word $(OUT)/HOL-SMT
-$(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy SMT/SMT.thy \
- SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
- SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \
- SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \
- SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \
- SMT/Tools/z3_proof_terms.ML SMT/Tools/z3_proof_rules.ML \
- SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML \
- SMT/Tools/z3_solver.ML
+$(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy \
+ SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
+ SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \
+ SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \
+ SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \
+ SMT/Tools/z3_proof_terms.ML SMT/Tools/z3_proof_rules.ML \
+ SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML \
+ SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
@@ -1161,203 +1144,157 @@
HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz
-$(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \
- SMT/Examples/SMT_Examples.thy \
- SMT/Examples/cert/z3_arith_quant_01 \
- SMT/Examples/cert/z3_arith_quant_01.proof \
- SMT/Examples/cert/z3_arith_quant_02 \
- SMT/Examples/cert/z3_arith_quant_02.proof \
- SMT/Examples/cert/z3_arith_quant_03 \
- SMT/Examples/cert/z3_arith_quant_03.proof \
- SMT/Examples/cert/z3_arith_quant_04 \
- SMT/Examples/cert/z3_arith_quant_04.proof \
- SMT/Examples/cert/z3_arith_quant_05 \
- SMT/Examples/cert/z3_arith_quant_05.proof \
- SMT/Examples/cert/z3_arith_quant_06 \
- SMT/Examples/cert/z3_arith_quant_06.proof \
- SMT/Examples/cert/z3_arith_quant_07 \
- SMT/Examples/cert/z3_arith_quant_07.proof \
- SMT/Examples/cert/z3_arith_quant_08 \
- SMT/Examples/cert/z3_arith_quant_08.proof \
- SMT/Examples/cert/z3_arith_quant_09 \
- SMT/Examples/cert/z3_arith_quant_09.proof \
- SMT/Examples/cert/z3_arith_quant_10 \
- SMT/Examples/cert/z3_arith_quant_10.proof \
- SMT/Examples/cert/z3_arith_quant_11 \
- SMT/Examples/cert/z3_arith_quant_11.proof \
- SMT/Examples/cert/z3_arith_quant_12 \
- SMT/Examples/cert/z3_arith_quant_12.proof \
- SMT/Examples/cert/z3_arith_quant_13 \
- SMT/Examples/cert/z3_arith_quant_13.proof \
- SMT/Examples/cert/z3_arith_quant_14 \
- SMT/Examples/cert/z3_arith_quant_14.proof \
- SMT/Examples/cert/z3_arith_quant_15 \
- SMT/Examples/cert/z3_arith_quant_15.proof \
- SMT/Examples/cert/z3_arith_quant_16 \
- SMT/Examples/cert/z3_arith_quant_16.proof \
- SMT/Examples/cert/z3_arith_quant_17 \
- SMT/Examples/cert/z3_arith_quant_17.proof \
- SMT/Examples/cert/z3_arith_quant_18 \
- SMT/Examples/cert/z3_arith_quant_18.proof \
- SMT/Examples/cert/z3_bv_01 \
- SMT/Examples/cert/z3_bv_01.proof \
- SMT/Examples/cert/z3_bv_02 \
- SMT/Examples/cert/z3_bv_02.proof \
- SMT/Examples/cert/z3_bv_arith_01 \
- SMT/Examples/cert/z3_bv_arith_01.proof \
- SMT/Examples/cert/z3_bv_arith_02 \
- SMT/Examples/cert/z3_bv_arith_02.proof \
- SMT/Examples/cert/z3_bv_arith_03 \
- SMT/Examples/cert/z3_bv_arith_03.proof \
- SMT/Examples/cert/z3_bv_arith_04 \
- SMT/Examples/cert/z3_bv_arith_04.proof \
- SMT/Examples/cert/z3_bv_arith_05 \
- SMT/Examples/cert/z3_bv_arith_05.proof \
- SMT/Examples/cert/z3_bv_arith_06 \
- SMT/Examples/cert/z3_bv_arith_06.proof \
- SMT/Examples/cert/z3_bv_arith_07 \
- SMT/Examples/cert/z3_bv_arith_07.proof \
- SMT/Examples/cert/z3_bv_arith_08 \
- SMT/Examples/cert/z3_bv_arith_08.proof \
- SMT/Examples/cert/z3_bv_arith_09 \
- SMT/Examples/cert/z3_bv_arith_09.proof \
- SMT/Examples/cert/z3_bv_arith_10 \
- SMT/Examples/cert/z3_bv_arith_10.proof \
- SMT/Examples/cert/z3_bv_bit_01 \
- SMT/Examples/cert/z3_bv_bit_01.proof \
- SMT/Examples/cert/z3_bv_bit_02 \
- SMT/Examples/cert/z3_bv_bit_02.proof \
- SMT/Examples/cert/z3_bv_bit_03 \
- SMT/Examples/cert/z3_bv_bit_03.proof \
- SMT/Examples/cert/z3_bv_bit_04 \
- SMT/Examples/cert/z3_bv_bit_04.proof \
- SMT/Examples/cert/z3_bv_bit_05 \
- SMT/Examples/cert/z3_bv_bit_05.proof \
- SMT/Examples/cert/z3_bv_bit_06 \
- SMT/Examples/cert/z3_bv_bit_06.proof \
- SMT/Examples/cert/z3_bv_bit_07 \
- SMT/Examples/cert/z3_bv_bit_07.proof \
- SMT/Examples/cert/z3_bv_bit_08 \
- SMT/Examples/cert/z3_bv_bit_08.proof \
- SMT/Examples/cert/z3_bv_bit_09 \
- SMT/Examples/cert/z3_bv_bit_09.proof \
- SMT/Examples/cert/z3_bv_bit_10 \
- SMT/Examples/cert/z3_bv_bit_10.proof \
- SMT/Examples/cert/z3_bv_bit_11 \
- SMT/Examples/cert/z3_bv_bit_11.proof \
- SMT/Examples/cert/z3_bv_bit_12 \
- SMT/Examples/cert/z3_bv_bit_12.proof \
- SMT/Examples/cert/z3_bv_bit_13 \
- SMT/Examples/cert/z3_bv_bit_13.proof \
- SMT/Examples/cert/z3_bv_bit_14 \
- SMT/Examples/cert/z3_bv_bit_14.proof \
- SMT/Examples/cert/z3_bv_bit_15 \
- SMT/Examples/cert/z3_bv_bit_15.proof \
- SMT/Examples/cert/z3_fol_01 \
- SMT/Examples/cert/z3_fol_01.proof \
- SMT/Examples/cert/z3_fol_02 \
- SMT/Examples/cert/z3_fol_02.proof \
- SMT/Examples/cert/z3_fol_03 \
- SMT/Examples/cert/z3_fol_03.proof \
- SMT/Examples/cert/z3_fol_04 \
- SMT/Examples/cert/z3_fol_04.proof \
- SMT/Examples/cert/z3_hol_01 \
- SMT/Examples/cert/z3_hol_01.proof \
- SMT/Examples/cert/z3_hol_02 \
- SMT/Examples/cert/z3_hol_02.proof \
- SMT/Examples/cert/z3_hol_03 \
- SMT/Examples/cert/z3_hol_03.proof \
- SMT/Examples/cert/z3_hol_04 \
- SMT/Examples/cert/z3_hol_04.proof \
- SMT/Examples/cert/z3_hol_05 \
- SMT/Examples/cert/z3_hol_05.proof \
- SMT/Examples/cert/z3_hol_06 \
- SMT/Examples/cert/z3_hol_06.proof \
- SMT/Examples/cert/z3_hol_07 \
- SMT/Examples/cert/z3_hol_07.proof \
- SMT/Examples/cert/z3_hol_08 \
- SMT/Examples/cert/z3_hol_08.proof \
- SMT/Examples/cert/z3_linarith_01 \
- SMT/Examples/cert/z3_linarith_01.proof \
- SMT/Examples/cert/z3_linarith_02 \
- SMT/Examples/cert/z3_linarith_02.proof \
- SMT/Examples/cert/z3_linarith_03 \
- SMT/Examples/cert/z3_linarith_03.proof \
- SMT/Examples/cert/z3_linarith_04 \
- SMT/Examples/cert/z3_linarith_04.proof \
- SMT/Examples/cert/z3_linarith_05 \
- SMT/Examples/cert/z3_linarith_05.proof \
- SMT/Examples/cert/z3_linarith_06 \
- SMT/Examples/cert/z3_linarith_06.proof \
- SMT/Examples/cert/z3_linarith_07 \
- SMT/Examples/cert/z3_linarith_07.proof \
- SMT/Examples/cert/z3_linarith_08 \
- SMT/Examples/cert/z3_linarith_08.proof \
- SMT/Examples/cert/z3_linarith_09 \
- SMT/Examples/cert/z3_linarith_09.proof \
- SMT/Examples/cert/z3_linarith_10 \
- SMT/Examples/cert/z3_linarith_10.proof \
- SMT/Examples/cert/z3_linarith_11 \
- SMT/Examples/cert/z3_linarith_11.proof \
- SMT/Examples/cert/z3_linarith_12 \
- SMT/Examples/cert/z3_linarith_12.proof \
- SMT/Examples/cert/z3_linarith_13 \
- SMT/Examples/cert/z3_linarith_13.proof \
- SMT/Examples/cert/z3_linarith_14 \
- SMT/Examples/cert/z3_linarith_14.proof \
- SMT/Examples/cert/z3_linarith_15 \
- SMT/Examples/cert/z3_linarith_15.proof \
- SMT/Examples/cert/z3_linarith_16 \
- SMT/Examples/cert/z3_linarith_16.proof \
- SMT/Examples/cert/z3_mono_01 \
- SMT/Examples/cert/z3_mono_01.proof \
- SMT/Examples/cert/z3_mono_02 \
- SMT/Examples/cert/z3_mono_02.proof \
- SMT/Examples/cert/z3_nat_arith_01 \
- SMT/Examples/cert/z3_nat_arith_01.proof \
- SMT/Examples/cert/z3_nat_arith_02 \
- SMT/Examples/cert/z3_nat_arith_02.proof \
- SMT/Examples/cert/z3_nat_arith_03 \
- SMT/Examples/cert/z3_nat_arith_03.proof \
- SMT/Examples/cert/z3_nat_arith_04 \
- SMT/Examples/cert/z3_nat_arith_04.proof \
- SMT/Examples/cert/z3_nat_arith_05 \
- SMT/Examples/cert/z3_nat_arith_05.proof \
- SMT/Examples/cert/z3_nat_arith_06 \
- SMT/Examples/cert/z3_nat_arith_06.proof \
- SMT/Examples/cert/z3_nat_arith_07 \
- SMT/Examples/cert/z3_nat_arith_07.proof \
- SMT/Examples/cert/z3_nlarith_01 \
- SMT/Examples/cert/z3_nlarith_01.proof \
- SMT/Examples/cert/z3_nlarith_02 \
- SMT/Examples/cert/z3_nlarith_02.proof \
- SMT/Examples/cert/z3_nlarith_03 \
- SMT/Examples/cert/z3_nlarith_03.proof \
- SMT/Examples/cert/z3_nlarith_04 \
- SMT/Examples/cert/z3_nlarith_04.proof \
- SMT/Examples/cert/z3_pair_01 \
- SMT/Examples/cert/z3_pair_01.proof \
- SMT/Examples/cert/z3_pair_02 \
- SMT/Examples/cert/z3_pair_02.proof \
- SMT/Examples/cert/z3_prop_01 \
- SMT/Examples/cert/z3_prop_01.proof \
- SMT/Examples/cert/z3_prop_02 \
- SMT/Examples/cert/z3_prop_02.proof \
- SMT/Examples/cert/z3_prop_03 \
- SMT/Examples/cert/z3_prop_03.proof \
- SMT/Examples/cert/z3_prop_04 \
- SMT/Examples/cert/z3_prop_04.proof \
- SMT/Examples/cert/z3_prop_05 \
- SMT/Examples/cert/z3_prop_05.proof \
- SMT/Examples/cert/z3_prop_06 \
- SMT/Examples/cert/z3_prop_06.proof \
- SMT/Examples/cert/z3_prop_07 \
- SMT/Examples/cert/z3_prop_07.proof \
- SMT/Examples/cert/z3_prop_08 \
- SMT/Examples/cert/z3_prop_08.proof \
- SMT/Examples/cert/z3_prop_09 \
- SMT/Examples/cert/z3_prop_09.proof \
- SMT/Examples/cert/z3_prop_10 \
+$(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \
+ SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01 \
+ SMT/Examples/cert/z3_arith_quant_01.proof \
+ SMT/Examples/cert/z3_arith_quant_02 \
+ SMT/Examples/cert/z3_arith_quant_02.proof \
+ SMT/Examples/cert/z3_arith_quant_03 \
+ SMT/Examples/cert/z3_arith_quant_03.proof \
+ SMT/Examples/cert/z3_arith_quant_04 \
+ SMT/Examples/cert/z3_arith_quant_04.proof \
+ SMT/Examples/cert/z3_arith_quant_05 \
+ SMT/Examples/cert/z3_arith_quant_05.proof \
+ SMT/Examples/cert/z3_arith_quant_06 \
+ SMT/Examples/cert/z3_arith_quant_06.proof \
+ SMT/Examples/cert/z3_arith_quant_07 \
+ SMT/Examples/cert/z3_arith_quant_07.proof \
+ SMT/Examples/cert/z3_arith_quant_08 \
+ SMT/Examples/cert/z3_arith_quant_08.proof \
+ SMT/Examples/cert/z3_arith_quant_09 \
+ SMT/Examples/cert/z3_arith_quant_09.proof \
+ SMT/Examples/cert/z3_arith_quant_10 \
+ SMT/Examples/cert/z3_arith_quant_10.proof \
+ SMT/Examples/cert/z3_arith_quant_11 \
+ SMT/Examples/cert/z3_arith_quant_11.proof \
+ SMT/Examples/cert/z3_arith_quant_12 \
+ SMT/Examples/cert/z3_arith_quant_12.proof \
+ SMT/Examples/cert/z3_arith_quant_13 \
+ SMT/Examples/cert/z3_arith_quant_13.proof \
+ SMT/Examples/cert/z3_arith_quant_14 \
+ SMT/Examples/cert/z3_arith_quant_14.proof \
+ SMT/Examples/cert/z3_arith_quant_15 \
+ SMT/Examples/cert/z3_arith_quant_15.proof \
+ SMT/Examples/cert/z3_arith_quant_16 \
+ SMT/Examples/cert/z3_arith_quant_16.proof \
+ SMT/Examples/cert/z3_arith_quant_17 \
+ SMT/Examples/cert/z3_arith_quant_17.proof \
+ SMT/Examples/cert/z3_arith_quant_18 \
+ SMT/Examples/cert/z3_arith_quant_18.proof SMT/Examples/cert/z3_bv_01 \
+ SMT/Examples/cert/z3_bv_01.proof SMT/Examples/cert/z3_bv_02 \
+ SMT/Examples/cert/z3_bv_02.proof SMT/Examples/cert/z3_bv_arith_01 \
+ SMT/Examples/cert/z3_bv_arith_01.proof \
+ SMT/Examples/cert/z3_bv_arith_02 \
+ SMT/Examples/cert/z3_bv_arith_02.proof \
+ SMT/Examples/cert/z3_bv_arith_03 \
+ SMT/Examples/cert/z3_bv_arith_03.proof \
+ SMT/Examples/cert/z3_bv_arith_04 \
+ SMT/Examples/cert/z3_bv_arith_04.proof \
+ SMT/Examples/cert/z3_bv_arith_05 \
+ SMT/Examples/cert/z3_bv_arith_05.proof \
+ SMT/Examples/cert/z3_bv_arith_06 \
+ SMT/Examples/cert/z3_bv_arith_06.proof \
+ SMT/Examples/cert/z3_bv_arith_07 \
+ SMT/Examples/cert/z3_bv_arith_07.proof \
+ SMT/Examples/cert/z3_bv_arith_08 \
+ SMT/Examples/cert/z3_bv_arith_08.proof \
+ SMT/Examples/cert/z3_bv_arith_09 \
+ SMT/Examples/cert/z3_bv_arith_09.proof \
+ SMT/Examples/cert/z3_bv_arith_10 \
+ SMT/Examples/cert/z3_bv_arith_10.proof \
+ SMT/Examples/cert/z3_bv_bit_01 SMT/Examples/cert/z3_bv_bit_01.proof \
+ SMT/Examples/cert/z3_bv_bit_02 SMT/Examples/cert/z3_bv_bit_02.proof \
+ SMT/Examples/cert/z3_bv_bit_03 SMT/Examples/cert/z3_bv_bit_03.proof \
+ SMT/Examples/cert/z3_bv_bit_04 SMT/Examples/cert/z3_bv_bit_04.proof \
+ SMT/Examples/cert/z3_bv_bit_05 SMT/Examples/cert/z3_bv_bit_05.proof \
+ SMT/Examples/cert/z3_bv_bit_06 SMT/Examples/cert/z3_bv_bit_06.proof \
+ SMT/Examples/cert/z3_bv_bit_07 SMT/Examples/cert/z3_bv_bit_07.proof \
+ SMT/Examples/cert/z3_bv_bit_08 SMT/Examples/cert/z3_bv_bit_08.proof \
+ SMT/Examples/cert/z3_bv_bit_09 SMT/Examples/cert/z3_bv_bit_09.proof \
+ SMT/Examples/cert/z3_bv_bit_10 SMT/Examples/cert/z3_bv_bit_10.proof \
+ SMT/Examples/cert/z3_bv_bit_11 SMT/Examples/cert/z3_bv_bit_11.proof \
+ SMT/Examples/cert/z3_bv_bit_12 SMT/Examples/cert/z3_bv_bit_12.proof \
+ SMT/Examples/cert/z3_bv_bit_13 SMT/Examples/cert/z3_bv_bit_13.proof \
+ SMT/Examples/cert/z3_bv_bit_14 SMT/Examples/cert/z3_bv_bit_14.proof \
+ SMT/Examples/cert/z3_bv_bit_15 SMT/Examples/cert/z3_bv_bit_15.proof \
+ SMT/Examples/cert/z3_fol_01 SMT/Examples/cert/z3_fol_01.proof \
+ SMT/Examples/cert/z3_fol_02 SMT/Examples/cert/z3_fol_02.proof \
+ SMT/Examples/cert/z3_fol_03 SMT/Examples/cert/z3_fol_03.proof \
+ SMT/Examples/cert/z3_fol_04 SMT/Examples/cert/z3_fol_04.proof \
+ SMT/Examples/cert/z3_hol_01 SMT/Examples/cert/z3_hol_01.proof \
+ SMT/Examples/cert/z3_hol_02 SMT/Examples/cert/z3_hol_02.proof \
+ SMT/Examples/cert/z3_hol_03 SMT/Examples/cert/z3_hol_03.proof \
+ SMT/Examples/cert/z3_hol_04 SMT/Examples/cert/z3_hol_04.proof \
+ SMT/Examples/cert/z3_hol_05 SMT/Examples/cert/z3_hol_05.proof \
+ SMT/Examples/cert/z3_hol_06 SMT/Examples/cert/z3_hol_06.proof \
+ SMT/Examples/cert/z3_hol_07 SMT/Examples/cert/z3_hol_07.proof \
+ SMT/Examples/cert/z3_hol_08 SMT/Examples/cert/z3_hol_08.proof \
+ SMT/Examples/cert/z3_linarith_01 \
+ SMT/Examples/cert/z3_linarith_01.proof \
+ SMT/Examples/cert/z3_linarith_02 \
+ SMT/Examples/cert/z3_linarith_02.proof \
+ SMT/Examples/cert/z3_linarith_03 \
+ SMT/Examples/cert/z3_linarith_03.proof \
+ SMT/Examples/cert/z3_linarith_04 \
+ SMT/Examples/cert/z3_linarith_04.proof \
+ SMT/Examples/cert/z3_linarith_05 \
+ SMT/Examples/cert/z3_linarith_05.proof \
+ SMT/Examples/cert/z3_linarith_06 \
+ SMT/Examples/cert/z3_linarith_06.proof \
+ SMT/Examples/cert/z3_linarith_07 \
+ SMT/Examples/cert/z3_linarith_07.proof \
+ SMT/Examples/cert/z3_linarith_08 \
+ SMT/Examples/cert/z3_linarith_08.proof \
+ SMT/Examples/cert/z3_linarith_09 \
+ SMT/Examples/cert/z3_linarith_09.proof \
+ SMT/Examples/cert/z3_linarith_10 \
+ SMT/Examples/cert/z3_linarith_10.proof \
+ SMT/Examples/cert/z3_linarith_11 \
+ SMT/Examples/cert/z3_linarith_11.proof \
+ SMT/Examples/cert/z3_linarith_12 \
+ SMT/Examples/cert/z3_linarith_12.proof \
+ SMT/Examples/cert/z3_linarith_13 \
+ SMT/Examples/cert/z3_linarith_13.proof \
+ SMT/Examples/cert/z3_linarith_14 \
+ SMT/Examples/cert/z3_linarith_14.proof \
+ SMT/Examples/cert/z3_linarith_15 \
+ SMT/Examples/cert/z3_linarith_15.proof \
+ SMT/Examples/cert/z3_linarith_16 \
+ SMT/Examples/cert/z3_linarith_16.proof SMT/Examples/cert/z3_mono_01 \
+ SMT/Examples/cert/z3_mono_01.proof SMT/Examples/cert/z3_mono_02 \
+ SMT/Examples/cert/z3_mono_02.proof SMT/Examples/cert/z3_nat_arith_01 \
+ SMT/Examples/cert/z3_nat_arith_01.proof \
+ SMT/Examples/cert/z3_nat_arith_02 \
+ SMT/Examples/cert/z3_nat_arith_02.proof \
+ SMT/Examples/cert/z3_nat_arith_03 \
+ SMT/Examples/cert/z3_nat_arith_03.proof \
+ SMT/Examples/cert/z3_nat_arith_04 \
+ SMT/Examples/cert/z3_nat_arith_04.proof \
+ SMT/Examples/cert/z3_nat_arith_05 \
+ SMT/Examples/cert/z3_nat_arith_05.proof \
+ SMT/Examples/cert/z3_nat_arith_06 \
+ SMT/Examples/cert/z3_nat_arith_06.proof \
+ SMT/Examples/cert/z3_nat_arith_07 \
+ SMT/Examples/cert/z3_nat_arith_07.proof \
+ SMT/Examples/cert/z3_nlarith_01 \
+ SMT/Examples/cert/z3_nlarith_01.proof \
+ SMT/Examples/cert/z3_nlarith_02 \
+ SMT/Examples/cert/z3_nlarith_02.proof \
+ SMT/Examples/cert/z3_nlarith_03 \
+ SMT/Examples/cert/z3_nlarith_03.proof \
+ SMT/Examples/cert/z3_nlarith_04 \
+ SMT/Examples/cert/z3_nlarith_04.proof SMT/Examples/cert/z3_pair_01 \
+ SMT/Examples/cert/z3_pair_01.proof SMT/Examples/cert/z3_pair_02 \
+ SMT/Examples/cert/z3_pair_02.proof SMT/Examples/cert/z3_prop_01 \
+ SMT/Examples/cert/z3_prop_01.proof SMT/Examples/cert/z3_prop_02 \
+ SMT/Examples/cert/z3_prop_02.proof SMT/Examples/cert/z3_prop_03 \
+ SMT/Examples/cert/z3_prop_03.proof SMT/Examples/cert/z3_prop_04 \
+ SMT/Examples/cert/z3_prop_04.proof SMT/Examples/cert/z3_prop_05 \
+ SMT/Examples/cert/z3_prop_05.proof SMT/Examples/cert/z3_prop_06 \
+ SMT/Examples/cert/z3_prop_06.proof SMT/Examples/cert/z3_prop_07 \
+ SMT/Examples/cert/z3_prop_07.proof SMT/Examples/cert/z3_prop_08 \
+ SMT/Examples/cert/z3_prop_08.proof SMT/Examples/cert/z3_prop_09 \
+ SMT/Examples/cert/z3_prop_09.proof SMT/Examples/cert/z3_prop_10 \
SMT/Examples/cert/z3_prop_10.proof
@cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples