equal
deleted
inserted
replaced
304 RealDef.thy \ |
304 RealDef.thy \ |
305 RealPow.thy \ |
305 RealPow.thy \ |
306 Real.thy \ |
306 Real.thy \ |
307 RealVector.thy \ |
307 RealVector.thy \ |
308 Tools/float_syntax.ML \ |
308 Tools/float_syntax.ML \ |
309 Tools/transfer_data.ML \ |
309 Tools/transfer.ML \ |
310 Tools/Qelim/ferrante_rackoff_data.ML \ |
310 Tools/Qelim/ferrante_rackoff_data.ML \ |
311 Tools/Qelim/ferrante_rackoff.ML \ |
311 Tools/Qelim/ferrante_rackoff.ML \ |
312 Tools/Qelim/langford_data.ML \ |
312 Tools/Qelim/langford_data.ML \ |
313 Tools/Qelim/langford.ML |
313 Tools/Qelim/langford.ML |
314 @$(ISABELLE_TOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL |
314 @$(ISABELLE_TOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL |
899 ex/Quickcheck_Examples.thy ex/ROOT.ML \ |
899 ex/Quickcheck_Examples.thy ex/ROOT.ML \ |
900 ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ |
900 ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ |
901 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
901 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
902 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ |
902 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ |
903 ex/Sudoku.thy ex/Tarski.thy \ |
903 ex/Sudoku.thy ex/Tarski.thy \ |
904 ex/Termination.thy ex/Unification.thy ex/document/root.bib \ |
904 ex/Termination.thy ex/Transfer_Ex.thy ex/Unification.thy ex/document/root.bib \ |
905 ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ |
905 ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ |
906 ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy |
906 ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy |
907 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
907 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
908 |
908 |
909 |
909 |