#
3dba35c1 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs, to allow unfold_abs_def;
|
#
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
#
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
#
90c1e718 |
|
06-Mar-2015 |
wenzelm <none@none> |
proper 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;
|
#
3ff7fdf2 |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
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;
|
#
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
#
8aa502e5 |
|
12-Jan-2014 |
wenzelm <none@none> |
tuned signature; clarified context;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
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;
|
#
3d5f7d6a |
|
10-Jan-2011 |
wenzelm <none@none> |
added merge_options convenience;
|
#
14d00fc2 |
|
12-Dec-2010 |
krauss <none@none> |
tuned headers
|
#
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;
|
#
e51cb1e7 |
|
05-Oct-2010 |
krauss <none@none> |
removed complicated (and rarely helpful) error reporting
|
#
d94c1a87 |
|
05-Oct-2010 |
krauss <none@none> |
discontinued continuations to simplify control flow; dropped optimization in scnp
|
#
dbf9b53f |
|
05-Oct-2010 |
krauss <none@none> |
use Cache structure instead of passing tables around explicitly
|
#
3e123ba2 |
|
26-Aug-2010 |
wenzelm <none@none> |
theory data merge: prefer left side uniformly;
|
#
266cf630 |
|
28-Apr-2010 |
krauss <none@none> |
default termination prover as plain tactic
|
#
7c7ac3fa |
|
07-Mar-2010 |
wenzelm <none@none> |
modernized structure Local_Defs;
|
#
15e88558 |
|
02-Jan-2010 |
krauss <none@none> |
absorb structures Decompose and Descent into Termination, to simplify further restructuring
|
#
4678ef3f |
|
23-Nov-2009 |
krauss <none@none> |
eliminated dead code and some unused bindings, reported by polyml
|
#
71833c27 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Theory_Data; tuned;
|
#
09f82753 |
|
06-Nov-2009 |
krauss <none@none> |
renamed method sizechange to size_change
|
#
e147f721 |
|
29-Oct-2009 |
krauss <none@none> |
less verbose termination tactics
|
#
56ef143d |
|
29-Oct-2009 |
blanchet <none@none> |
make "sizechange_tac" slightly less verbose
|
#
f8850b31 |
|
23-Oct-2009 |
krauss <none@none> |
function package: more standard names for structures and files
|
#
50da8ae7 |
|
22-Oct-2009 |
haftmann <none@none> |
map_range (and map_index) combinator
|
#
d103ca85 |
|
21-Oct-2009 |
haftmann <none@none> |
removed old-style \ and \\ infixes
|
#
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;
|
#
eb69614d |
|
15-Oct-2009 |
wenzelm <none@none> |
normalized aliases of Output operations;
|
#
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;
|
#
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
|