| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
da18404a |
|
22-Feb-2018 |
wenzelm <none@none> |
tuned;
|
| #
3257c050 |
|
21-Dec-2016 |
blanchet <none@none> |
moved and exported tactic
|
| #
b97bf4c0 |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
09941e1d |
|
14-Feb-2016 |
blanchet <none@none> |
tuning
|
| #
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;
|
| #
591a7bfe |
|
01-Dec-2015 |
blanchet <none@none> |
tuned whitespace
|
| #
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
839d9ae3 |
|
26-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
|
| #
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
86dff2b5 |
|
16-Jul-2015 |
blanchet <none@none> |
made tactic more robust w.r.t. equations containing 'case_prod'
|
| #
dbbe37ca |
|
15-Jul-2015 |
traytel <none@none> |
{r,e,d,f}tac with proper context in BNF
|
| #
8d25dfd8 |
|
03-May-2015 |
blanchet <none@none> |
made split-rule tactic go beyond constructors with 20 arguments
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
8d8391a8 |
|
05-Mar-2015 |
blanchet <none@none> |
strengthened tactic
|
| #
676428c4 |
|
05-Mar-2015 |
blanchet <none@none> |
strengthened tactic
|
| #
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;
|
| #
1f391ad1 |
|
19-Dec-2014 |
desharna <none@none> |
use proper context in function
|
| #
d6623f99 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
| #
6fb4e52a |
|
18-Aug-2014 |
blanchet <none@none> |
reordered some (co)datatype property names for more consistency
|
| #
c1bd04e5 |
|
27-Jun-2014 |
blanchet <none@none> |
compile
|
| #
7c886e63 |
|
18-Jun-2014 |
blanchet <none@none> |
made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
|
| #
da328fb3 |
|
07-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
| #
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
| #
c0de7553 |
|
05-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
fd5d98a4 |
|
05-Feb-2014 |
blanchet <none@none> |
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
|
| #
88a2727e |
|
20-Jan-2014 |
blanchet <none@none> |
tuned names
|
| #
e8e169dd |
|
20-Jan-2014 |
blanchet <none@none> |
adjusted comments
|
| #
a0868967 |
|
20-Jan-2014 |
blanchet <none@none> |
avoid nested 'Tools' directories
--HG--
rename : src/HOL/Tools/BNF/Tools/bnf_comp.ML => src/HOL/Tools/BNF/bnf_comp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_comp_tactics.ML => src/HOL/Tools/BNF/bnf_comp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_def.ML => src/HOL/Tools/BNF/bnf_def.ML
rename : src/HOL/Tools/BNF/Tools/bnf_def_tactics.ML => src/HOL/Tools/BNF/bnf_def_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar.ML => src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar_tactics.ML => src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m.ML => src/HOL/Tools/BNF/bnf_fp_n2m.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m_sugar.ML => src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m_tactics.ML => src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_rec_sugar_util.ML => src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_util.ML => src/HOL/Tools/BNF/bnf_fp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp.ML => src/HOL/Tools/BNF/bnf_gfp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar.ML => src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML => src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_tactics.ML => src/HOL/Tools/BNF/bnf_gfp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_util.ML => src/HOL/Tools/BNF/bnf_gfp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp.ML => src/HOL/Tools/BNF/bnf_lfp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_compat.ML => src/HOL/Tools/BNF/bnf_lfp_compat.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_rec_sugar.ML => src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_tactics.ML => src/HOL/Tools/BNF/bnf_lfp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_util.ML => src/HOL/Tools/BNF/bnf_lfp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_tactics.ML => src/HOL/Tools/BNF/bnf_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_util.ML => src/HOL/Tools/BNF/bnf_util.ML
|