#
3fe8d55b |
|
12-Nov-2013 |
blanchet <none@none> |
ported part of function package to new 'Ctr_Sugar' abstraction
|
#
d0858517 |
|
12-Nov-2013 |
blanchet <none@none> |
undid copy-paste
|
#
d3a207ad |
|
27-Apr-2011 |
wenzelm <none@none> |
eliminated obsolete Function_Lib.frees_in_term; simplified;
|
#
342b80ce |
|
16-Apr-2011 |
wenzelm <none@none> |
observe firm naming convention ctxt: Proof.context;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
14d00fc2 |
|
12-Dec-2010 |
krauss <none@none> |
tuned headers
|
#
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
|
#
f8850b31 |
|
23-Oct-2009 |
krauss <none@none> |
function package: more standard names for structures and files
|
#
8eb709ab |
|
20-Oct-2009 |
haftmann <none@none> |
curried inter as canonical list operation (beware of argument order)
|
#
8de45ab6 |
|
21-Oct-2009 |
haftmann <none@none> |
dropped redundant gen_ prefix
|
#
68478f6d |
|
20-Oct-2009 |
haftmann <none@none> |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
#
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;
|
#
d9aef710 |
|
17-Jul-2009 |
wenzelm <none@none> |
tuned/modernized Envir.subst_XXX;
|
#
d0b33b8e |
|
23-Jun-2009 |
haftmann <none@none> |
tuned interfaces of datatype module
|
#
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
|