| #
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
| #
3dba35c1 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs, to allow unfold_abs_def;
|
| #
20bd4bda |
|
18-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
| #
9d926c7e |
|
18-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
| #
c7340223 |
|
17-Apr-2016 |
wenzelm <none@none> |
prefer binding over base name;
|
| #
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
| #
952abf53 |
|
06-Sep-2015 |
wenzelm <none@none> |
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
|
| #
bc3d393f |
|
16-Aug-2015 |
wenzelm <none@none> |
added Thm.chyps_of;
eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
|
| #
a804eb03 |
|
05-Jul-2015 |
wenzelm <none@none> |
clarified context;
|
| #
4ed536e2 |
|
30-May-2015 |
wenzelm <none@none> |
tuned;
|
| #
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
4b4960a7 |
|
08-Mar-2015 |
wenzelm <none@none> |
misc tuning and simplification;
|
| #
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;
|
| #
b7bf58e6 |
|
03-Mar-2015 |
traytel <none@none> |
eliminated some clones of Proof_Context.cterm_of
|
| #
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
| #
c7eb8d77 |
|
28-Jan-2015 |
eberlm <none@none> |
Fixed bug in bugfix for function package
|
| #
e7984da9 |
|
27-Jan-2015 |
eberlm <none@none> |
Fixed variable naming bug in function package
|
| #
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
| #
147d4ad6 |
|
07-Mar-2014 |
blanchet <none@none> |
tuning
|
| #
db965533 |
|
10-Jan-2014 |
wenzelm <none@none> |
more elementary management of declared hyps, below structure Assumption;
Goal.prove: insist in declared hyps;
Simplifier: declare hyps via Thm.assume_hyps;
more accurate tool context in some boundary cases;
|
| #
f83d74cd |
|
23-Nov-2013 |
wenzelm <none@none> |
more accurate goal context;
|
| #
5ae4a26b |
|
08-Sep-2013 |
krauss <none@none> |
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
normalized whitespace and indentation
|
| #
e19b5371 |
|
08-Sep-2013 |
krauss <none@none> |
clarified
|
| #
5fd3c443 |
|
08-Sep-2013 |
krauss <none@none> |
clarified, dropping unreachable bool special case
|
| #
f8580d36 |
|
08-Sep-2013 |
krauss <none@none> |
dropped dead code
|
| #
68e03336 |
|
08-Sep-2013 |
Manuel Eberl <none@none> |
generate elim rules for elimination of function equalities;
added fun_cases command;
recover proper cases rules for mutual recursive case (no sum types)
|
| #
6e401e29 |
|
16-Jun-2013 |
krauss <none@none> |
export dom predicate in the info record
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
62ec754a |
|
13-Mar-2012 |
wenzelm <none@none> |
more explicit indication of def names;
|
| #
476fb08c |
|
08-Nov-2011 |
wenzelm <none@none> |
tuned;
|
| #
9d72cd6f |
|
27-Apr-2011 |
krauss <none@none> |
inlined Function_Lib.replace_frees, which is used only once
|
| #
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
| #
8caff1de |
|
25-Feb-2011 |
krauss <none@none> |
removed support for tail-recursion from function package (now implemented by partial_function)
|
| #
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;
|
| #
0dc105bc |
|
22-Oct-2010 |
krauss <none@none> |
some cleanup in Function_Lib
|
| #
a00eb206 |
|
27-Sep-2010 |
krauss <none@none> |
consolidated tupled_lambda; moved to structure HOLogic
|
| #
a1f58d52 |
|
10-Sep-2010 |
krauss <none@none> |
improved error message for common mistake (fun f where "g x = ...")
|
| #
dc514061 |
|
15-May-2010 |
wenzelm <none@none> |
less pervasive names from structure Thm;
|
| #
0d3b744a |
|
09-May-2010 |
krauss <none@none> |
do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings
|
| #
7c7ac3fa |
|
07-Mar-2010 |
wenzelm <none@none> |
modernized structure Local_Defs;
|
| #
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
|
| #
8d32b36e |
|
19-Nov-2009 |
wenzelm <none@none> |
adapted Local_Theory.define -- eliminated odd thm kind;
|
| #
d28e2372 |
|
13-Nov-2009 |
wenzelm <none@none> |
modernized structure Local_Theory;
|
| #
d4527641 |
|
12-Nov-2009 |
wenzelm <none@none> |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
| #
d75378a4 |
|
02-Nov-2009 |
krauss <none@none> |
do not use Binding.empty: conceal flag gets lost in Thm.def_binding_optional
|
| #
346742c9 |
|
28-Oct-2009 |
wenzelm <none@none> |
simplified default binding;
conceal internal bindings;
|
| #
f8850b31 |
|
23-Oct-2009 |
krauss <none@none> |
function package: more standard names for structures and files
|
| #
8518a24a |
|
29-Sep-2009 |
wenzelm <none@none> |
modernized Balanced_Tree;
|
| #
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;
|
| #
dde326d7 |
|
17-Jul-2009 |
wenzelm <none@none> |
compare types directly -- no need to invoke Type.eq_type with empty environment;
|
| #
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
|