#
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
#
7aae2956 |
|
25-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate; tuned;
|
#
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
#
a7d3b0ad |
|
07-Jul-2015 |
blanchet <none@none> |
have the installed termination prover take a 'quiet' flag
|
#
53f968f4 |
|
01-Jun-2015 |
wenzelm <none@none> |
clarified context;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
45f9fa0b |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
de8e2f0e |
|
19-Dec-2014 |
wenzelm <none@none> |
just one data slot per program unit; tuned signature;
|
#
6d42cd2f |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup; tuned whitespace;
|
#
9067b570 |
|
16-Aug-2014 |
wenzelm <none@none> |
updated to named_theorems; modernized module name and setup;
|
#
f5593ebf |
|
20-Mar-2014 |
wenzelm <none@none> |
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
|
#
4332fea6 |
|
12-May-2013 |
wenzelm <none@none> |
retain goal display options when printing error messages, to avoid breakdown for huge goals;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
3e959f21 |
|
15-Oct-2012 |
wenzelm <none@none> |
tuned message -- avoid extra blank lines;
|
#
a3b9e251 |
|
13-Oct-2012 |
wenzelm <none@none> |
some attempts to unify/simplify pretty_goal;
|
#
7601cf1a |
|
12-Apr-2012 |
wenzelm <none@none> |
more standard method setup;
|
#
941cf8eb |
|
02-Dec-2011 |
wenzelm <none@none> |
more antiquotations;
|
#
14ffc3e9 |
|
13-May-2011 |
wenzelm <none@none> |
clarified map_simpset versus Simplifier.map_simpset_global;
|
#
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
|
#
19985150 |
|
12-May-2011 |
wenzelm <none@none> |
prefer plain simpset operations;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
d1e89721 |
|
13-Jan-2011 |
wenzelm <none@none> |
more precise pretty printing -- to accomodate Scala message layout;
|
#
046d8672 |
|
03-Nov-2010 |
wenzelm <none@none> |
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
|
#
cad9c456 |
|
05-Oct-2010 |
krauss <none@none> |
tuned
|
#
039a09ca |
|
05-Oct-2010 |
krauss <none@none> |
force less agressively
|
#
72823114 |
|
05-Oct-2010 |
krauss <none@none> |
lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
|
#
3319b478 |
|
03-Sep-2010 |
wenzelm <none@none> |
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
|
#
266cf630 |
|
28-Apr-2010 |
krauss <none@none> |
default termination prover as plain tactic
|
#
5e512ec7 |
|
27-Feb-2010 |
wenzelm <none@none> |
clarified @{const_name} vs. @{const_abbrev};
|
#
75f69d99 |
|
10-Feb-2010 |
haftmann <none@none> |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
#
7b3a0878 |
|
28-Jan-2010 |
haftmann <none@none> |
new theory Algebras.thy for generic algebraic structures
|
#
eb23531d |
|
02-Jan-2010 |
krauss <none@none> |
new year's resolution: reindented code in function package
|
#
4678ef3f |
|
23-Nov-2009 |
krauss <none@none> |
eliminated dead code and some unused bindings, reported by polyml
|
#
274fded3 |
|
02-Nov-2009 |
krauss <none@none> |
lexicographic order: run local descent proofs in parallel
|
#
e147f721 |
|
29-Oct-2009 |
krauss <none@none> |
less verbose termination tactics
|
#
f8850b31 |
|
23-Oct-2009 |
krauss <none@none> |
function package: more standard names for structures and files
|
#
75401f7b |
|
15-Oct-2009 |
wenzelm <none@none> |
replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
|
#
37b6b840 |
|
18-Sep-2009 |
haftmann <none@none> |
tuned const_name antiquotations
|
#
db497781 |
|
25-Jul-2009 |
wenzelm <none@none> |
renamed structure Display_Goal to Goal_Display; --HG-- rename : src/Pure/display_goal.ML => src/Pure/goal_display.ML
|
#
c9446e75 |
|
24-Jul-2009 |
wenzelm <none@none> |
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
|
#
a4b600c4 |
|
23-Jul-2009 |
wenzelm <none@none> |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
#
268732d9 |
|
23-Jul-2009 |
wenzelm <none@none> |
clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
|
#
0fb8f22f |
|
20-Jul-2009 |
wenzelm <none@none> |
moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
|
#
7b41de27 |
|
02-Jul-2009 |
wenzelm <none@none> |
renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
|
#
d18d6a07 |
|
22-Jun-2009 |
haftmann <none@none> |
uniformly capitialized names for subdirectories --HG-- rename : src/HOL/Tools/datatype_package/datatype.ML => src/HOL/Tools/Datatype/datatype.ML rename : src/HOL/Tools/datatype_package/datatype_abs_proofs.ML => src/HOL/Tools/Datatype/datatype_abs_proofs.ML rename : src/HOL/Tools/datatype_package/datatype_aux.ML => src/HOL/Tools/Datatype/datatype_aux.ML rename : src/HOL/Tools/datatype_package/datatype_case.ML => src/HOL/Tools/Datatype/datatype_case.ML rename : src/HOL/Tools/datatype_package/datatype_codegen.ML => src/HOL/Tools/Datatype/datatype_codegen.ML rename : src/HOL/Tools/datatype_package/datatype_prop.ML => src/HOL/Tools/Datatype/datatype_prop.ML rename : src/HOL/Tools/datatype_package/datatype_realizer.ML => src/HOL/Tools/Datatype/datatype_realizer.ML rename : src/HOL/Tools/datatype_package/datatype_rep_proofs.ML => src/HOL/Tools/Datatype/datatype_rep_proofs.ML rename : src/HOL/Tools/function_package/auto_term.ML => src/HOL/Tools/Function/auto_term.ML rename : src/HOL/Tools/function_package/context_tree.ML => src/HOL/Tools/Function/context_tree.ML rename : src/HOL/Tools/function_package/decompose.ML => src/HOL/Tools/Function/decompose.ML rename : src/HOL/Tools/function_package/descent.ML => src/HOL/Tools/Function/descent.ML rename : src/HOL/Tools/function_package/fundef.ML => src/HOL/Tools/Function/fundef.ML rename : src/HOL/Tools/function_package/fundef_common.ML => src/HOL/Tools/Function/fundef_common.ML rename : src/HOL/Tools/function_package/fundef_core.ML => src/HOL/Tools/Function/fundef_core.ML rename : src/HOL/Tools/function_package/fundef_datatype.ML => src/HOL/Tools/Function/fundef_datatype.ML rename : src/HOL/Tools/function_package/fundef_lib.ML => src/HOL/Tools/Function/fundef_lib.ML rename : src/HOL/Tools/function_package/induction_scheme.ML => src/HOL/Tools/Function/induction_scheme.ML rename : src/HOL/Tools/function_package/inductive_wrap.ML => src/HOL/Tools/Function/inductive_wrap.ML rename : src/HOL/Tools/function_package/lexicographic_order.ML => src/HOL/Tools/Function/lexicographic_order.ML rename : src/HOL/Tools/function_package/measure_functions.ML => src/HOL/Tools/Function/measure_functions.ML rename : src/HOL/Tools/function_package/mutual.ML => src/HOL/Tools/Function/mutual.ML rename : src/HOL/Tools/function_package/pattern_split.ML => src/HOL/Tools/Function/pattern_split.ML rename : src/HOL/Tools/function_package/scnp_reconstruct.ML => src/HOL/Tools/Function/scnp_reconstruct.ML rename : src/HOL/Tools/function_package/scnp_solve.ML => src/HOL/Tools/Function/scnp_solve.ML rename : src/HOL/Tools/function_package/size.ML => src/HOL/Tools/Function/size.ML rename : src/HOL/Tools/function_package/sum_tree.ML => src/HOL/Tools/Function/sum_tree.ML rename : src/HOL/Tools/function_package/termination.ML => src/HOL/Tools/Function/termination.ML rename : src/Tools/code/code_haskell.ML => src/Tools/Code/code_haskell.ML rename : src/Tools/code/code_ml.ML => src/Tools/Code/code_ml.ML rename : src/Tools/code/code_preproc.ML => src/Tools/Code/code_preproc.ML rename : src/Tools/code/code_printer.ML => src/Tools/Code/code_printer.ML rename : src/Tools/code/code_target.ML => src/Tools/Code/code_target.ML rename : src/Tools/code/code_thingol.ML => src/Tools/Code/code_thingol.ML
|