| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
17fc044a |
|
01-Feb-2018 |
wenzelm <none@none> |
clarified signature;
|
| #
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
2759308d |
|
25-Sep-2015 |
wenzelm <none@none> |
moved remaining display.ML to more_thm.ML;
|
| #
bc3d393f |
|
16-Aug-2015 |
wenzelm <none@none> |
added Thm.chyps_of;
eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
|
| #
9a9cf694 |
|
05-Jul-2015 |
wenzelm <none@none> |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
| #
65c57129 |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
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;
|
| #
e3153e9f |
|
11-Jan-2015 |
wenzelm <none@none> |
tuned warnings: observe Context_Position.is_visible;
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
233ef912 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
| #
80c18f3e |
|
04-May-2014 |
blanchet <none@none> |
tuned structure name
|
| #
1efc2078 |
|
04-May-2014 |
blanchet <none@none> |
renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
|
| #
7399e785 |
|
04-May-2014 |
blanchet <none@none> |
make 'dpll_p' the default SAT solver, rather than the hard-to-get zChaff-with-proofs
|
| #
edea2531 |
|
01-May-2014 |
boehmes <none@none> |
less verbose SAT tactic
|
| #
da328fb3 |
|
07-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
| #
1d0205f7 |
|
01-Feb-2014 |
wenzelm <none@none> |
proper config options;
proper context for printing;
|
| #
42a54449 |
|
01-Feb-2014 |
wenzelm <none@none> |
more standard file/module names;
--HG--
rename : src/HOL/Tools/cnf_funcs.ML => src/HOL/Tools/cnf.ML
rename : src/HOL/Tools/sat_funcs.ML => src/HOL/Tools/sat.ML
|