Rewrite the Probability theory.
Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
#
# IsaMakefile for HOL
#
## targets
default: HOL
generate: HOL-Generate-HOL HOL-Generate-HOLLight
images: \
HOL \
HOL-Library \
HOL-Algebra \
HOL-Boogie \
HOL-Multivariate_Analysis \
HOL-NSA \
HOL-Nominal \
HOL-Probability \
HOL-Proofs \
HOL-Word \
HOL4 \
TLA \
HOL-Base \
HOL-Main \
HOL-Plain
#Note: keep targets sorted (except for HOL-ex)
test: \
HOL-ex \
HOL-Auth \
HOL-Bali \
HOL-Boogie-Examples \
HOL-Decision_Procs \
HOL-Hahn_Banach \
HOL-Hoare \
HOL-Hoare_Parallel \
HOL-IMP \
HOL-IMPP \
HOL-IOA \
HOL-Imperative_HOL \
HOL-Import \
HOL-Induct \
HOL-Isar_Examples \
HOL-Lattice \
HOL-Library-Codegenerator_Test \
HOL-Matrix \
HOL-Metis_Examples \
HOL-MicroJava \
HOL-Mirabelle \
HOL-Mutabelle \
HOL-NanoJava \
HOL-Nitpick_Examples \
HOL-Nominal-Examples \
HOL-Number_Theory \
HOL-Old_Number_Theory \
HOL-Quotient_Examples \
HOL-Predicate_Compile_Examples \
HOL-Prolog \
HOL-Proofs-Extraction \
HOL-Proofs-Lambda \
HOL-SET_Protocol \
HOL-Word-SMT_Examples \
HOL-Statespace \
HOL-Subst \
TLA-Buffer \
TLA-Inc \
TLA-Memory \
HOL-UNITY \
HOL-Unix \
HOL-Word-Examples \
HOL-ZF
# ^ this is the sort position
all: test images
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
## HOL
HOL: Pure $(OUT)/HOL
HOL-Base: Pure $(OUT)/HOL-Base
HOL-Plain: Pure $(OUT)/HOL-Plain
HOL-Main: Pure $(OUT)/HOL-Main
HOL-Proofs: Pure $(OUT)/HOL-Proofs
Pure:
@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
$(OUT)/Pure: Pure
BASE_DEPENDENCIES = $(OUT)/Pure \
$(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML \
$(SRC)/Provers/classical.ML \
$(SRC)/Provers/hypsubst.ML \
$(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/splitter.ML \
$(SRC)/Tools/cache_io.ML \
$(SRC)/Tools/Code/code_eval.ML \
$(SRC)/Tools/Code/code_haskell.ML \
$(SRC)/Tools/Code/code_ml.ML \
$(SRC)/Tools/Code/code_preproc.ML \
$(SRC)/Tools/Code/code_printer.ML \
$(SRC)/Tools/Code/code_scala.ML \
$(SRC)/Tools/Code/code_simp.ML \
$(SRC)/Tools/Code/code_target.ML \
$(SRC)/Tools/Code/code_thingol.ML \
$(SRC)/Tools/Code_Generator.thy \
$(SRC)/Tools/IsaPlanner/isand.ML \
$(SRC)/Tools/IsaPlanner/rw_inst.ML \
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/zipper.ML \
$(SRC)/Tools/atomize_elim.ML \
$(SRC)/Tools/auto_counterexample.ML \
$(SRC)/Tools/auto_solve.ML \
$(SRC)/Tools/coherent.ML \
$(SRC)/Tools/cong_tac.ML \
$(SRC)/Tools/eqsubst.ML \
$(SRC)/Tools/induct.ML \
$(SRC)/Tools/induct_tacs.ML \
$(SRC)/Tools/intuitionistic.ML \
$(SRC)/Tools/misc_legacy.ML \
$(SRC)/Tools/nbe.ML \
$(SRC)/Tools/project_rule.ML \
$(SRC)/Tools/quickcheck.ML \
$(SRC)/Tools/random_word.ML \
$(SRC)/Tools/value.ML \
HOL.thy \
Tools/hologic.ML \
Tools/recfun_codegen.ML \
Tools/simpdata.ML
$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
Complete_Lattice.thy \
Datatype.thy \
Extraction.thy \
Fields.thy \
Finite_Set.thy \
Fun.thy \
FunDef.thy \
Groups.thy \
Inductive.thy \
Lattices.thy \
Nat.thy \
Option.thy \
Orderings.thy \
Plain.thy \
Power.thy \
Predicate.thy \
Product_Type.thy \
Record.thy \
Relation.thy \
Rings.thy \
SAT.thy \
Set.thy \
Sum_Type.thy \
Tools/abel_cancel.ML \
Tools/arith_data.ML \
Tools/cnf_funcs.ML \
Tools/Datatype/datatype_abs_proofs.ML \
Tools/Datatype/datatype_aux.ML \
Tools/Datatype/datatype_case.ML \
Tools/Datatype/datatype_codegen.ML \
Tools/Datatype/datatype_data.ML \
Tools/Datatype/datatype_prop.ML \
Tools/Datatype/datatype_realizer.ML \
Tools/Datatype/datatype.ML \
Tools/dseq.ML \
Tools/Function/context_tree.ML \
Tools/Function/function_common.ML \
Tools/Function/function_core.ML \
Tools/Function/function_lib.ML \
Tools/Function/function.ML \
Tools/Function/fun.ML \
Tools/Function/induction_schema.ML \
Tools/Function/lexicographic_order.ML \
Tools/Function/measure_functions.ML \
Tools/Function/mutual.ML \
Tools/Function/pat_completeness.ML \
Tools/Function/pattern_split.ML \
Tools/Function/relation.ML \
Tools/Function/scnp_reconstruct.ML \
Tools/Function/scnp_solve.ML \
Tools/Function/size.ML \
Tools/Function/sum_tree.ML \
Tools/Function/termination.ML \
Tools/inductive_codegen.ML \
Tools/inductive.ML \
Tools/inductive_realizer.ML \
Tools/inductive_set.ML \
Tools/lin_arith.ML \
Tools/nat_arith.ML \
Tools/old_primrec.ML \
Tools/primrec.ML \
Tools/prop_logic.ML \
Tools/refute.ML \
Tools/refute_isar.ML \
Tools/rewrite_hol_proof.ML \
Tools/sat_funcs.ML \
Tools/sat_solver.ML \
Tools/split_rule.ML \
Tools/typedef.ML \
Transitive_Closure.thy \
Typedef.thy \
Wellfounded.thy \
$(SRC)/Provers/Arith/cancel_div_mod.ML \
$(SRC)/Provers/Arith/cancel_sums.ML \
$(SRC)/Provers/Arith/fast_lin_arith.ML \
$(SRC)/Provers/order.ML \
$(SRC)/Provers/trancl.ML \
$(SRC)/Tools/rat.ML
$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
Big_Operators.thy \
Code_Evaluation.thy \
Code_Numeral.thy \
Divides.thy \
DSequence.thy \
Equiv_Relations.thy \
Groebner_Basis.thy \
Hilbert_Choice.thy \
Int.thy \
Lazy_Sequence.thy \
List.thy \
Main.thy \
Map.thy \
Nat_Numeral.thy \
Nat_Transfer.thy \
Nitpick.thy \
Numeral_Simprocs.thy \
Presburger.thy \
Predicate_Compile.thy \
Quickcheck.thy \
Quotient.thy \
Random.thy \
Random_Sequence.thy \
Recdef.thy \
Refute.thy \
Semiring_Normalization.thy \
SetInterval.thy \
Sledgehammer.thy \
SMT.thy \
String.thy \
Typerep.thy \
$(SRC)/Provers/Arith/assoc_fold.ML \
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
$(SRC)/Provers/Arith/cancel_numerals.ML \
$(SRC)/Provers/Arith/combine_numerals.ML \
$(SRC)/Provers/Arith/extract_common_term.ML \
$(SRC)/Tools/Metis/metis.ML \
Tools/ATP/async_manager.ML \
Tools/ATP/atp_problem.ML \
Tools/ATP/atp_systems.ML \
Tools/choice_specification.ML \
Tools/int_arith.ML \
Tools/groebner.ML \
Tools/list_code.ML \
Tools/meson.ML \
Tools/nat_numeral_simprocs.ML \
Tools/Nitpick/kodkod.ML \
Tools/Nitpick/kodkod_sat.ML \
Tools/Nitpick/minipick.ML \
Tools/Nitpick/nitpick.ML \
Tools/Nitpick/nitpick_hol.ML \
Tools/Nitpick/nitpick_isar.ML \
Tools/Nitpick/nitpick_kodkod.ML \
Tools/Nitpick/nitpick_model.ML \
Tools/Nitpick/nitpick_mono.ML \
Tools/Nitpick/nitpick_nut.ML \
Tools/Nitpick/nitpick_peephole.ML \
Tools/Nitpick/nitpick_preproc.ML \
Tools/Nitpick/nitpick_rep.ML \
Tools/Nitpick/nitpick_scope.ML \
Tools/Nitpick/nitpick_tests.ML \
Tools/Nitpick/nitpick_util.ML \
Tools/numeral.ML \
Tools/numeral_simprocs.ML \
Tools/numeral_syntax.ML \
Tools/Predicate_Compile/predicate_compile_aux.ML \
Tools/Predicate_Compile/predicate_compile_compilations.ML \
Tools/Predicate_Compile/predicate_compile_core.ML \
Tools/Predicate_Compile/predicate_compile_data.ML \
Tools/Predicate_Compile/predicate_compile_fun.ML \
Tools/Predicate_Compile/predicate_compile.ML \
Tools/Predicate_Compile/predicate_compile_specialisation.ML \
Tools/Predicate_Compile/predicate_compile_pred.ML \
Tools/quickcheck_generators.ML \
Tools/Qelim/cooper.ML \
Tools/Qelim/cooper_procedure.ML \
Tools/Qelim/qelim.ML \
Tools/Quotient/quotient_def.ML \
Tools/Quotient/quotient_info.ML \
Tools/Quotient/quotient_tacs.ML \
Tools/Quotient/quotient_term.ML \
Tools/Quotient/quotient_typ.ML \
Tools/recdef.ML \
Tools/record.ML \
Tools/semiring_normalizer.ML \
Tools/Sledgehammer/clausifier.ML \
Tools/Sledgehammer/meson_tactic.ML \
Tools/Sledgehammer/metis_clauses.ML \
Tools/Sledgehammer/metis_tactics.ML \
Tools/Sledgehammer/sledgehammer.ML \
Tools/Sledgehammer/sledgehammer_fact_filter.ML \
Tools/Sledgehammer/sledgehammer_fact_minimize.ML \
Tools/Sledgehammer/sledgehammer_isar.ML \
Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
Tools/Sledgehammer/sledgehammer_translate.ML \
Tools/Sledgehammer/sledgehammer_util.ML \
Tools/SMT/cvc3_solver.ML \
Tools/SMT/smtlib_interface.ML \
Tools/SMT/smt_monomorph.ML \
Tools/SMT/smt_normalize.ML \
Tools/SMT/smt_solver.ML \
Tools/SMT/smt_translate.ML \
Tools/SMT/yices_solver.ML \
Tools/SMT/z3_interface.ML \
Tools/SMT/z3_model.ML \
Tools/SMT/z3_proof_literals.ML \
Tools/SMT/z3_proof_parser.ML \
Tools/SMT/z3_proof_reconstruction.ML \
Tools/SMT/z3_proof_tools.ML \
Tools/SMT/z3_solver.ML \
Tools/string_code.ML \
Tools/string_syntax.ML \
Tools/transfer.ML \
Tools/TFL/casesplit.ML \
Tools/TFL/dcterm.ML \
Tools/TFL/post.ML \
Tools/TFL/rules.ML \
Tools/TFL/tfl.ML \
Tools/TFL/thms.ML \
Tools/TFL/thry.ML \
Tools/TFL/usyntax.ML \
Tools/TFL/utils.ML
$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
Archimedean_Field.thy \
Complex.thy \
Complex_Main.thy \
Deriv.thy \
Fact.thy \
GCD.thy \
Lim.thy \
Limits.thy \
Ln.thy \
Log.thy \
Lubs.thy \
MacLaurin.thy \
NthRoot.thy \
Parity.thy \
RComplete.thy \
Rat.thy \
Real.thy \
RealDef.thy \
RealVector.thy \
SEQ.thy \
Series.thy \
SupInf.thy \
Taylor.thy \
Transcendental.thy \
Tools/float_syntax.ML \
Tools/SMT/smt_real.ML
$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
## HOL-Library
HOL-Library: HOL $(OUT)/HOL-Library
$(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML \
$(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \
Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \
Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \
Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
Library/Code_Integer.thy Library/Code_Natural.thy \
Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \
Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \
Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \
Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy \
Library/Executable_Set.thy Library/Float.thy \
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy \
Library/Function_Algebras.thy \
Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \
Library/Indicator_Function.thy Library/Infinite_Set.thy \
Library/Inner_Product.thy Library/Kleene_Algebra.thy \
Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \
Library/Lattice_Syntax.thy Library/Library.thy \
Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \
Library/Multiset.thy Library/Nat_Bijection.thy \
Library/Nat_Infinity.thy Library/Nested_Environment.thy \
Library/Numeral_Type.thy Library/OptionalSugar.thy \
Library/Order_Relation.thy Library/Permutation.thy \
Library/Permutations.thy Library/Poly_Deriv.thy \
Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \
Library/Preorder.thy Library/Product_Vector.thy \
Library/Product_ord.thy Library/Product_plus.thy \
Library/Quickcheck_Types.thy Library/Quicksort.thy \
Library/Quotient_List.thy Library/Quotient_Option.thy \
Library/Quotient_Product.thy Library/Quotient_Sum.thy \
Library/Quotient_Syntax.thy Library/Quotient_Type.thy \
Library/RBT.thy Library/RBT_Impl.thy Library/README.html \
Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \
Library/Reflection.thy Library/SML_Quickcheck.thy \
Library/Sublist_Order.thy Library/Sum_Of_Squares.thy \
Library/Sum_Of_Squares/sos_wrapper.ML \
Library/Sum_Of_Squares/sum_of_squares.ML \
Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
Library/While_Combinator.thy Library/Zorn.thy \
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \
Library/reflection.ML Library/reify_data.ML \
Library/document/root.bib Library/document/root.tex
@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
## HOL-Hahn_Banach
HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz
$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy \
Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy \
Hahn_Banach/Hahn_Banach.thy Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy \
Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy \
Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html \
Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy \
Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy \
Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
## HOL-Subst
HOL-Subst: HOL $(LOG)/HOL-Subst.gz
$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML \
Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
## HOL-Induct
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \
Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy \
Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \
Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy \
Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
## HOL-IMP
HOL-IMP: HOL $(LOG)/HOL-IMP.gz
$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy \
IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \
IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy \
IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
## HOL-IMPP
HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \
IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
## HOL-Import
IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \
Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
Import/hol4rews.ML Import/import.ML Import/ROOT.ML
IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
Import/hol4rews.ML Import/import.ML Import/ROOT.ML
HOL-Import: HOL $(LOG)/HOL-Import.gz
$(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
@$(ISABELLE_TOOL) usedir -p 0 $(OUT)/HOL Import
## HOL-Generate-HOL
HOL-Generate-HOL: HOL $(LOG)/HOL-Generate-HOL.gz
$(LOG)/HOL-Generate-HOL.gz: $(OUT)/HOL \
$(IMPORTER_FILES) Import/Generate-HOL/GenHOL4Base.thy \
Import/Generate-HOL/GenHOL4Prob.thy \
Import/Generate-HOL/GenHOL4Real.thy \
Import/Generate-HOL/GenHOL4Vec.thy \
Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOL
## HOL-Generate-HOLLight
HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz
$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL \
$(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy \
Import/Generate-HOLLight/ROOT.ML
@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight
## HOL-Import-HOL
HOL4: HOL $(LOG)/HOL4.gz
HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \
bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
hrat.imp hreal.imp ind_type.imp lim.imp list.imp marker.imp nets.imp \
numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \
powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \
prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \
prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \
rich_list.imp \
seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
word_base.imp word_bitop.imp word_num.imp
$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES) \
$(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \
Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy \
Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy \
Import/HOL/ROOT.ML
@cd Import/HOL; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL4
HOLLight: HOL $(LOG)/HOLLight.gz
$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES) \
Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \
Import/HOLLight/ROOT.ML
@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
## HOL-Number_Theory
HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
Library/Multiset.thy \
Number_Theory/Binomial.thy \
Number_Theory/Cong.thy \
Number_Theory/Fib.thy \
Number_Theory/MiscAlgebra.thy \
Number_Theory/Number_Theory.thy \
Number_Theory/Residues.thy \
Number_Theory/UniqueFactorization.thy \
Number_Theory/ROOT.ML
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory
## HOL-Old_Number_Theory
HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \
Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \
Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\
Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \
Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \
Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \
Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \
Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \
Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \
Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \
Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy \
Old_Number_Theory/ROOT.ML
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
## HOL-Hoare
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \
Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy \
Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \
Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \
Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \
Hoare/SchorrWaite.thy Hoare/Separation.thy \
Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
## HOL-Hoare_Parallel
HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz
$(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy \
Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy \
Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy \
Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy \
Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy \
Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy \
Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy \
Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy \
Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML \
Hoare_Parallel/document/root.tex Hoare_Parallel/document/root.bib
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel
## HOL-Library-Codegenerator_Test
HOL-Library-Codegenerator_Test: HOL-Library $(LOG)/HOL-Library-Codegenerator_Test.gz
$(LOG)/HOL-Library-Codegenerator_Test.gz: $(OUT)/HOL-Library \
Codegenerator_Test/ROOT.ML \
Codegenerator_Test/Candidates.thy \
Codegenerator_Test/Candidates_Pretty.thy \
Codegenerator_Test/Generate.thy \
Codegenerator_Test/Generate_Pretty.thy
@$(ISABELLE_TOOL) usedir -d false -g false -i false $(OUT)/HOL-Library Codegenerator_Test
## HOL-Metis_Examples
HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
Metis_Examples/BT.thy Metis_Examples/Message.thy \
Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
Metis_Examples/set.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
## HOL-Nitpick_Examples
HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
Nitpick_Examples/Typedef_Nits.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
## HOL-Algebra
HOL-Algebra: HOL $(OUT)/HOL-Algebra
ALGEBRA_DEPENDENCIES = $(OUT)/HOL \
Algebra/ROOT.ML \
Library/Binomial.thy \
Library/FuncSet.thy \
Library/Multiset.thy \
Library/Permutation.thy \
Number_Theory/Primes.thy \
Algebra/AbelCoset.thy \
Algebra/Bij.thy \
Algebra/Congruence.thy \
Algebra/Coset.thy \
Algebra/Divisibility.thy \
Algebra/Exponent.thy \
Algebra/FiniteProduct.thy \
Algebra/Group.thy \
Algebra/Ideal.thy \
Algebra/IntRing.thy \
Algebra/Lattice.thy \
Algebra/Module.thy \
Algebra/QuotRing.thy \
Algebra/Ring.thy \
Algebra/RingHom.thy \
Algebra/Sylow.thy \
Algebra/UnivPoly.thy \
Algebra/abstract/Abstract.thy \
Algebra/abstract/Factor.thy \
Algebra/abstract/Field.thy \
Algebra/abstract/Ideal2.thy \
Algebra/abstract/PID.thy \
Algebra/abstract/Ring2.thy \
Algebra/abstract/RingHomo.thy \
Algebra/document/root.tex \
Algebra/document/root.tex \
Algebra/poly/LongDiv.thy \
Algebra/poly/PolyHomo.thy \
Algebra/poly/Polynomial.thy \
Algebra/poly/UnivPoly2.thy \
Algebra/ringsimp.ML
$(OUT)/HOL-Algebra: $(ALGEBRA_DEPENDENCIES)
@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
## HOL-Auth
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
$(LOG)/HOL-Auth.gz: $(OUT)/HOL \
Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \
Auth/Guard/Auth_Guard_Shared.thy \
Auth/Guard/Auth_Guard_Public.thy \
Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \
Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \
Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \
Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \
Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy \
Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy \
Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy \
Auth/KerberosIV_Gets.thy Auth/KerberosV.thy Auth/Yahalom.thy \
Auth/Yahalom2.thy Auth/Yahalom_Bad.thy Auth/ZhouGollmann.thy \
Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \
Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \
Auth/Guard/P1.thy Auth/Guard/P2.thy Auth/Guard/Proto.thy \
Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy \
Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy \
Auth/Smartcard/Smartcard.thy Auth/document/root.tex
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth
## HOL-UNITY
HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
UNITY/UNITY_Main.thy UNITY/UNITY_Examples.thy UNITY/UNITY_tactics.ML \
UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy \
UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy \
UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \
UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy \
UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy \
UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy \
UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \
UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy \
UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy \
UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy \
UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \
UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \
UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \
UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
UNITY/Comp/TimerArray.thy UNITY/document/root.tex
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY
## HOL-Unix
HOL-Unix: HOL $(LOG)/HOL-Unix.gz
$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \
Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \
Unix/document/root.bib Unix/document/root.tex
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
## HOL-ZF
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \
ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
## HOL-Imperative_HOL
HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Array.thy \
Imperative_HOL/Heap.thy Imperative_HOL/Heap_Monad.thy \
Imperative_HOL/Imperative_HOL.thy Imperative_HOL/Imperative_HOL_ex.thy\
Imperative_HOL/Mrec.thy Imperative_HOL/Ref.thy \
Imperative_HOL/ex/Imperative_Quicksort.thy \
Imperative_HOL/ex/Imperative_Reverse.thy \
Imperative_HOL/ex/Linked_Lists.thy \
Imperative_HOL/ex/SatChecker.thy \
Imperative_HOL/ex/Sorted_List.thy \
Imperative_HOL/ex/Subarray.thy \
Imperative_HOL/ex/Sublist.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
## HOL-Decision_Procs
HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz
$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \
Decision_Procs/Approximation.thy \
Decision_Procs/Commutative_Ring.thy \
Decision_Procs/Commutative_Ring_Complete.thy \
Decision_Procs/Cooper.thy \
Decision_Procs/Decision_Procs.thy \
Decision_Procs/Dense_Linear_Order.thy \
Decision_Procs/Ferrack.thy \
Decision_Procs/MIR.thy \
Decision_Procs/Parametric_Ferrante_Rackoff.thy \
Decision_Procs/Polynomial_List.thy \
Decision_Procs/ROOT.ML \
Decision_Procs/Reflected_Multivariate_Polynomial.thy \
Decision_Procs/commutative_ring_tac.ML \
Decision_Procs/cooper_tac.ML \
Decision_Procs/ex/Approximation_Ex.thy \
Decision_Procs/ex/Commutative_Ring_Ex.thy \
Decision_Procs/ex/Dense_Linear_Order_Ex.thy \
Decision_Procs/ferrack_tac.ML \
Decision_Procs/ferrante_rackoff.ML \
Decision_Procs/ferrante_rackoff_data.ML \
Decision_Procs/langford.ML \
Decision_Procs/langford_data.ML \
Decision_Procs/mir_tac.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
## HOL-Docs
HOL-Docs: HOL $(LOG)/HOL-Docs.gz
$(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML \
Docs/document/root.tex
@$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs
## HOL-Proofs-Lambda
HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs Lambda/Commutation.thy \
Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy \
Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy \
Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex
@$(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
## HOL-Prolog
HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \
Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
## HOL-MicroJava
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \
MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy \
MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy \
MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy \
MicroJava/Comp/LemmasComp.thy MicroJava/Comp/NatCanonify.thy \
MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy \
MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy \
MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \
MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \
MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \
MicroJava/J/WellForm.thy MicroJava/J/Value.thy \
MicroJava/J/WellType.thy MicroJava/J/Example.thy \
MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy \
MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy \
MicroJava/JVM/JVMExecInstr.thy MicroJava/JVM/JVMListExample.thy \
MicroJava/JVM/JVMExceptions.thy MicroJava/DFA/Abstract_BV.thy \
MicroJava/DFA/Err.thy MicroJava/DFA/Kildall.thy \
MicroJava/DFA/LBVComplete.thy MicroJava/DFA/LBVCorrect.thy \
MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy \
MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy \
MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy \
MicroJava/DFA/Semilattices.thy MicroJava/DFA/Typing_Framework_err.thy \
MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy \
MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/Correct.thy \
MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy \
MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \
MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy \
MicroJava/BV/LBVJVM.thy MicroJava/document/root.bib \
MicroJava/document/root.tex MicroJava/document/introduction.tex
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava
## HOL-NanoJava
HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML NanoJava/Term.thy \
NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
NanoJava/document/root.bib NanoJava/document/root.tex
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava
## HOL-Bali
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
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
## HOL-Proofs-Extraction
HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \
Library/Efficient_Nat.thy Extraction/Euclid.thy \
Extraction/Greatest_Common_Divisor.thy Extraction/Higman.thy \
Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML \
Extraction/Util.thy Extraction/Warshall.thy \
Extraction/document/root.tex Extraction/document/root.bib
@$(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
## HOL-IOA
HOL-IOA: HOL $(LOG)/HOL-IOA.gz
$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML \
IOA/Solve.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
## HOL-Lattice
HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \
Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \
Lattice/ROOT.ML Lattice/document/root.tex
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice
## HOL-ex
HOL-ex: HOL $(LOG)/HOL-ex.gz
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
Number_Theory/Primes.thy \
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/Coherent.thy ex/Dedekind_Real.thy \
ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
ex/Gauge_Integration.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_Schema.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/Quickcheck_Lattice_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/Tree23.thy \
ex/Unification.thy ex/While_Combinator_Example.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
## HOL-Isar_Examples
HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz
$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy \
Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy \
Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \
Isar_Examples/Group.thy Isar_Examples/Hoare.thy \
Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \
Isar_Examples/Mutilated_Checkerboard.thy \
Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \
Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy \
Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty \
Isar_Examples/document/root.bib Isar_Examples/document/root.tex \
Isar_Examples/document/style.tex Hoare/hoare_tac.ML \
Number_Theory/Primes.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples
## HOL-SET_Protocol
HOL-SET_Protocol: HOL $(LOG)/HOL-SET_Protocol.gz
$(LOG)/HOL-SET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML \
SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy \
SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \
SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \
SET_Protocol/document/root.tex
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
## HOL-Matrix
HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
$(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ComputeFloat.thy \
Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy \
Matrix/Compute_Oracle/Compute_Oracle.thy Matrix/Compute_Oracle/am.ML \
Matrix/Compute_Oracle/am_compiler.ML Matrix/Compute_Oracle/am_ghc.ML \
Matrix/Compute_Oracle/am_interpreter.ML \
Matrix/Compute_Oracle/am_sml.ML Matrix/Compute_Oracle/compute.ML \
Matrix/Compute_Oracle/linker.ML Matrix/Cplex.thy \
Matrix/CplexMatrixConverter.ML Matrix/Cplex_tools.ML \
Matrix/FloatSparseMatrixBuilder.ML Matrix/LP.thy Matrix/Matrix.thy \
Matrix/ROOT.ML Matrix/SparseMatrix.thy Matrix/document/root.tex \
Matrix/fspmlp.ML Matrix/matrixlp.ML Tools/float_arith.ML
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix
## TLA
TLA: HOL $(OUT)/TLA
$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \
TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA
## TLA-Inc
TLA-Inc: TLA $(LOG)/TLA-Inc.gz
$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc
## TLA-Buffer
TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy \
TLA/Buffer/DBuffer.thy
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
## TLA-Memory
TLA-Memory: TLA $(LOG)/TLA-Memory.gz
$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MemClerk.thy \
TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.thy \
TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy \
TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy \
TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
## HOL-Multivariate_Analysis
HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis
$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL \
Multivariate_Analysis/Brouwer_Fixpoint.thy \
Multivariate_Analysis/Cartesian_Euclidean_Space.thy \
Multivariate_Analysis/Convex_Euclidean_Space.thy \
Multivariate_Analysis/Derivative.thy \
Multivariate_Analysis/Determinants.thy \
Multivariate_Analysis/Euclidean_Space.thy \
Multivariate_Analysis/Fashoda.thy \
Multivariate_Analysis/Finite_Cartesian_Product.thy \
Multivariate_Analysis/Integration.certs \
Multivariate_Analysis/Integration.thy \
Multivariate_Analysis/Gauge_Measure.thy \
Multivariate_Analysis/L2_Norm.thy \
Multivariate_Analysis/Multivariate_Analysis.thy \
Multivariate_Analysis/Operator_Norm.thy \
Multivariate_Analysis/Path_Connected.thy \
Multivariate_Analysis/ROOT.ML \
Multivariate_Analysis/Real_Integration.thy \
Multivariate_Analysis/Topology_Euclidean_Space.thy \
Multivariate_Analysis/document/root.tex \
Multivariate_Analysis/normarith.ML Library/Glbs.thy \
Library/Inner_Product.thy Library/Numeral_Type.thy \
Library/Convex.thy Library/FrechetDeriv.thy \
Library/Product_Vector.thy Library/Product_plus.thy
@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
## HOL-Probability
HOL-Probability: HOL-Multivariate_Analysis $(OUT)/HOL-Probability
$(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis Probability/ROOT.ML \
Probability/Probability.thy Probability/Sigma_Algebra.thy \
Probability/Caratheodory.thy \
Probability/Borel.thy Probability/Measure.thy \
Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy \
Probability/Positive_Infinite_Real.thy Probability/Product_Measure.thy \
Probability/Probability_Space.thy Probability/Information.thy \
Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy \
Probability/Lebesgue_Measure.thy \
Library/Nat_Bijection.thy Library/Countable.thy
@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability
## HOL-Nominal
HOL-Nominal: HOL $(OUT)/HOL-Nominal
$(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \
Nominal/Nominal.thy \
Nominal/nominal_atoms.ML \
Nominal/nominal_datatype.ML \
Nominal/nominal_fresh_fun.ML \
Nominal/nominal_induct.ML \
Nominal/nominal_inductive.ML \
Nominal/nominal_inductive2.ML \
Nominal/nominal_permeq.ML \
Nominal/nominal_primrec.ML \
Nominal/nominal_thmdecls.ML \
Library/Infinite_Set.thy
@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
## HOL-Nominal-Examples
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
Nominal/Examples/Nominal_Examples.thy \
Nominal/Examples/CK_Machine.thy \
Nominal/Examples/CR.thy \
Nominal/Examples/CR_Takahashi.thy \
Nominal/Examples/Class1.thy \
Nominal/Examples/Class2.thy \
Nominal/Examples/Class3.thy \
Nominal/Examples/Compile.thy \
Nominal/Examples/Contexts.thy \
Nominal/Examples/Crary.thy \
Nominal/Examples/Fsub.thy \
Nominal/Examples/Height.thy \
Nominal/Examples/Lam_Funs.thy \
Nominal/Examples/Lambda_mu.thy \
Nominal/Examples/LocalWeakening.thy \
Nominal/Examples/Pattern.thy \
Nominal/Examples/ROOT.ML \
Nominal/Examples/SN.thy \
Nominal/Examples/SOS.thy \
Nominal/Examples/Standardization.thy \
Nominal/Examples/Support.thy \
Nominal/Examples/Type_Preservation.thy \
Nominal/Examples/VC_Condition.thy \
Nominal/Examples/W.thy \
Nominal/Examples/Weakening.thy
@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples
## HOL-Word
HOL-Word: HOL $(OUT)/HOL-Word
$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy \
Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy \
Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy \
Word/Bool_List_Representation.thy Word/Bit_Operations.thy \
Word/Word.thy Word/document/root.tex \
Word/document/root.bib Tools/SMT/smt_word.ML
@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
## HOL-Word-Examples
HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz
$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML \
Word/Examples/WordExamples.thy
@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples
## HOL-Statespace
HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz
$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \
Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \
Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy \
Statespace/distinct_tree_prover.ML Statespace/state_space.ML \
Statespace/state_fun.ML Statespace/document/root.tex
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace
## HOL-NSA
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
@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
## HOL-NSA-Examples
HOL-NSA-Examples: HOL-NSA $(LOG)/HOL-NSA-Examples.gz
$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML \
NSA/Examples/NSPrimes.thy
@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
## HOL-Mirabelle
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 \
Mirabelle/Tools/mirabelle_sledgehammer.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
## HOL-Word-SMT_Examples
HOL-Word-SMT_Examples: HOL-Word $(LOG)/HOL-Word-SMT_Examples.gz
$(LOG)/HOL-Word-SMT_Examples.gz: $(OUT)/HOL-Word SMT_Examples/ROOT.ML \
SMT_Examples/SMT_Examples.thy SMT_Examples/SMT_Examples.certs \
SMT_Examples/SMT_Word_Examples.thy SMT_Examples/SMT_Tests.thy \
SMT_Examples/SMT_Word_Examples.certs SMT_Examples/SMT_Tests.certs
@$(ISABELLE_TOOL) usedir $(OUT)/HOL-Word SMT_Examples
## HOL-Boogie
HOL-Boogie: HOL-Word $(OUT)/HOL-Boogie
$(OUT)/HOL-Boogie: $(OUT)/HOL-Word Boogie/ROOT.ML Boogie/Boogie.thy \
Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \
Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_tactics.ML
@cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-Boogie
## HOL-Boogie_Examples
HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz
$(LOG)/HOL-Boogie-Examples.gz: $(OUT)/HOL-Boogie \
Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy \
Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy \
Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i \
Boogie/Examples/VCC_Max.b2i Boogie/Examples/Boogie_Max.certs \
Boogie/Examples/Boogie_Dijkstra.certs Boogie/Examples/VCC_Max.certs
@cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples
## HOL-Mutabelle
HOL-Mutabelle: HOL $(LOG)/HOL-Mutabelle.gz
$(LOG)/HOL-Mutabelle.gz: $(OUT)/HOL Mutabelle/MutabelleExtra.thy \
Mutabelle/ROOT.ML Mutabelle/mutabelle.ML \
Mutabelle/mutabelle_extra.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle
## HOL-Quotient_Examples
HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \
Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \
Quotient_Examples/Quotient_Message.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
## HOL-Predicate_Compile_Examples
HOL-Predicate_Compile_Examples: HOL $(LOG)/HOL-Predicate_Compile_Examples.gz
$(LOG)/HOL-Predicate_Compile_Examples.gz: $(OUT)/HOL \
Predicate_Compile_Examples/ROOT.ML \
Predicate_Compile_Examples/Predicate_Compile_Examples.thy \
Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \
Predicate_Compile_Examples/Code_Prolog_Examples.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
## clean
clean:
@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz \
$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz \
$(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz \
$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Hahn_Banach.gz \
$(LOG)/HOL-Hoare.gz $(LOG)/HOL-Hoare_Parallel.gz \
$(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz \
$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz \
$(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz \
$(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz \
$(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz \
$(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix \
$(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz \
$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz \
$(LOG)/HOL-Multivariate_Analysis.gz \
$(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz \
$(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz \
$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz \
$(LOG)/HOL-Number_Theory.gz \
$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz \
$(LOG)/HOL-Predicate_Compile_Examples.gz \
$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz \
$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-Extraction.gz \
$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \
$(LOG)/HOL-Word-SMT_Examples.gz \
$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \
$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \
$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \
$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \
$(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \
$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \
$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \
$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \
$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \
$(OUT)/HOL-Probability $(OUT)/HOL-Proofs \
$(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA