equal
deleted
inserted
replaced
15 by (erule contrapos_nn) (rule arg_cong) |
15 by (erule contrapos_nn) (rule arg_cong) |
16 |
16 |
17 ML_file "Tools/Sledgehammer/async_manager.ML" |
17 ML_file "Tools/Sledgehammer/async_manager.ML" |
18 ML_file "Tools/Sledgehammer/sledgehammer_util.ML" |
18 ML_file "Tools/Sledgehammer/sledgehammer_util.ML" |
19 ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" |
19 ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" |
20 ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML" |
20 ML_file "Tools/Sledgehammer/sledgehammer_proof_methods.ML" |
21 ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML" |
21 ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML" |
22 ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML" |
22 ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML" |
23 ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML" |
23 ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML" |
24 ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML" |
24 ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML" |
25 ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML" |
25 ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML" |