| #
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
|