465 Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \ |
465 Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \ |
466 Library/Reflection.thy Library/SML_Quickcheck.thy \ |
466 Library/Reflection.thy Library/SML_Quickcheck.thy \ |
467 Library/Sublist_Order.thy Library/Sum_of_Squares.thy \ |
467 Library/Sublist_Order.thy Library/Sum_of_Squares.thy \ |
468 Library/Sum_of_Squares/sos_wrapper.ML \ |
468 Library/Sum_of_Squares/sos_wrapper.ML \ |
469 Library/Sum_of_Squares/sum_of_squares.ML \ |
469 Library/Sum_of_Squares/sum_of_squares.ML \ |
470 Library/TPTP.thy Library/Transitive_Closure_Table.thy \ |
470 Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \ |
471 Library/Univ_Poly.thy Library/While_Combinator.thy Library/Zorn.thy \ |
471 Library/While_Combinator.thy Library/Zorn.thy \ |
472 $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ |
472 $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ |
473 Library/reflection.ML Library/reify_data.ML \ |
473 Library/reflection.ML Library/reify_data.ML \ |
474 Library/Quickcheck_Narrowing.thy \ |
474 Library/Quickcheck_Narrowing.thy \ |
475 Tools/Quickcheck/narrowing_generators.ML \ |
475 Tools/Quickcheck/narrowing_generators.ML \ |
476 Tools/Quickcheck/Narrowing_Engine.hs \ |
476 Tools/Quickcheck/Narrowing_Engine.hs \ |
1046 ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ |
1046 ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ |
1047 ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \ |
1047 ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \ |
1048 ex/Quickcheck_Narrowing_Examples.thy \ |
1048 ex/Quickcheck_Narrowing_Examples.thy \ |
1049 ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \ |
1049 ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \ |
1050 ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \ |
1050 ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \ |
1051 ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy ex/Sqrt.thy \ |
1051 ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \ |
|
1052 ex/sledgehammer_tactics.ML ex/Sqrt.thy \ |
1052 ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \ |
1053 ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \ |
1053 ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \ |
1054 ex/TPTP.thy ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \ |
1054 ex/While_Combinator_Example.thy ex/document/root.bib \ |
1055 ex/While_Combinator_Example.thy ex/document/root.bib \ |
1055 ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ |
1056 ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ |
1056 ../Tools/interpretation_with_defs.ML |
1057 ../Tools/interpretation_with_defs.ML |
1057 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
1058 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
1058 |
1059 |
1314 Mirabelle/Tools/mirabelle_metis.ML \ |
1315 Mirabelle/Tools/mirabelle_metis.ML \ |
1315 Mirabelle/Tools/mirabelle_quickcheck.ML \ |
1316 Mirabelle/Tools/mirabelle_quickcheck.ML \ |
1316 Mirabelle/Tools/mirabelle_refute.ML \ |
1317 Mirabelle/Tools/mirabelle_refute.ML \ |
1317 Mirabelle/Tools/mirabelle_sledgehammer.ML \ |
1318 Mirabelle/Tools/mirabelle_sledgehammer.ML \ |
1318 Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \ |
1319 Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \ |
1319 Mirabelle/Tools/sledgehammer_tactics.ML \ |
1320 ex/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \ |
1320 Mirabelle/lib/Tools/mirabelle Mirabelle/lib/scripts/mirabelle.pl \ |
1321 Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \ |
1321 Library/FrechetDeriv.thy Library/Inner_Product.thy |
1322 Library/Inner_Product.thy |
1322 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle |
1323 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle |
1323 @cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case |
1324 @cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case |
1324 |
1325 |
1325 |
1326 |
1326 ## HOL-Word-SMT_Examples |
1327 ## HOL-Word-SMT_Examples |