History log of /seL4-l4v-master/l4v/isabelle/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
Revision Date Author Comments
# c65dec0f 28-Oct-2016 blanchet <none@none>

adapted Nunchaku integration to keyword renaming
# 13ddea91 26-Nov-2014 wenzelm <none@none>

renamed "pairself" to "apply2", in accordance to @{apply 2};
# 85fd5f19 01-Jul-2014 blanchet <none@none>

robustness in the face of ill-typed "unchecked" terms (e.g. case expressions)
# 70573b75 03-Feb-2014 blanchet <none@none>

tuning
# 91ba1387 02-Feb-2014 blanchet <none@none>

reset timing information after changes
# 70b7915d 31-Jan-2014 blanchet <none@none>

tuned ML function names
# fed5d9bd 31-Jan-2014 blanchet <none@none>

tuning
# 06f3d979 30-Jan-2014 blanchet <none@none>

refactor large ML file
# eb52da60 31-Jan-2014 blanchet <none@none>

renamed many Sledgehammer ML files to clarify structure

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_run.ML => src/HOL/Tools/Sledgehammer/sledgehammer.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_print.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML