2008-07-15 |
wenzelm |
added command 'linear_undo';
|
file |
diff |
annotate
|
2008-07-14 |
haftmann |
unified curried gcd, lcm, zgcd, zlcm
|
file |
diff |
annotate
|
2008-07-11 |
haftmann |
Fract now total; improved code generator setup
|
file |
diff |
annotate
|
2008-07-10 |
wenzelm |
slightly improved @{lemma} (both for latex and ML);
|
file |
diff |
annotate
|
2008-07-04 |
huffman |
HOL-NSA
|
file |
diff |
annotate
|
2008-07-02 |
haftmann |
code antiquotation roaring ahead
|
file |
diff |
annotate
|
2008-07-01 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
2008-07-01 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
2008-06-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2008-06-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2008-06-28 |
wenzelm |
additional ML antiquotations;
|
file |
diff |
annotate
|
2008-06-28 |
wenzelm |
@{lemma}: 'by' keyword;
|
file |
diff |
annotate
|
2008-06-28 |
wenzelm |
ML: improved antiquotations;
|
file |
diff |
annotate
|
2008-06-23 |
wenzelm |
induct_tac: mutual rules work as for method "induct";
|
file |
diff |
annotate
|
2008-06-20 |
haftmann |
(removed non-present change)
|
file |
diff |
annotate
|
2008-06-19 |
wenzelm |
disposed Sign.read_typ etc;
|
file |
diff |
annotate
|
2008-06-18 |
wenzelm |
* Disposed old term read functions;
|
file |
diff |
annotate
|
2008-06-16 |
wenzelm |
* Rules and tactics that read instantiations now demand a proper context;
|
file |
diff |
annotate
|
2008-06-14 |
wenzelm |
removed exotic 'token_translation' command;
|
file |
diff |
annotate
|
2008-06-13 |
wenzelm |
* Recovered hiding of consts;
|
file |
diff |
annotate
|
2008-06-11 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2008-06-10 |
wenzelm |
tuned spacing;
|
file |
diff |
annotate
|
2008-06-10 |
wenzelm |
* Attributes cases, induct, coinduct support del option.
|
file |
diff |
annotate
|
2008-06-10 |
wenzelm |
proper news header;
|
file |
diff |
annotate
|
2008-06-10 |
haftmann |
rep_datatype command now takes list of constructors as input arguments
|
file |
diff |
annotate
|
2008-06-03 |
wenzelm |
some reorganization and fine-tuning;
|
file |
diff |
annotate
|
2008-06-02 |
wenzelm |
reorganized isar-ref;
|
file |
diff |
annotate
|
2008-05-28 |
wenzelm |
misc tuning for Isabelle2008;
|
file |
diff |
annotate
|
2008-05-21 |
berghofe |
Added entry explaining incompatibilities introduced by replacing sets by predicates.
|
file |
diff |
annotate
|
2008-05-18 |
wenzelm |
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
|
file |
diff |
annotate
|
2008-05-16 |
wenzelm |
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
|
file |
diff |
annotate
|
2008-05-15 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2008-05-15 |
wenzelm |
* Simplified pdfsetup.sty;
|
file |
diff |
annotate
|
2008-05-13 |
krauss |
NEWS about measure functions
|
file |
diff |
annotate
|
2008-05-12 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
2008-05-02 |
ballarin |
unfold_locales part of default method.
|
file |
diff |
annotate
|
2008-04-29 |
haftmann |
added lemma antiquotation
|
file |
diff |
annotate
|
2008-04-25 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
2008-04-19 |
wenzelm |
NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;
|
file |
diff |
annotate
|
2008-04-17 |
wenzelm |
* Context-dependent token translations.
|
file |
diff |
annotate
|
2008-04-16 |
berghofe |
Added entry for unused_thms command.
|
file |
diff |
annotate
|
2008-04-15 |
wenzelm |
added hide fact;
|
file |
diff |
annotate
|
2008-04-15 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2008-04-15 |
wenzelm |
* Name space merge now observes canonical order;
|
file |
diff |
annotate
|
2008-04-08 |
wenzelm |
support for YXML notation -- XML done right;
|
file |
diff |
annotate
|
2008-04-07 |
paulson |
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
|
file |
diff |
annotate
|
2008-04-02 |
haftmann |
explicit class "eq" for operational equality
|
file |
diff |
annotate
|
2008-03-30 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2008-03-29 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
file |
diff |
annotate
|
2008-03-29 |
wenzelm |
fixed spelling;
|
file |
diff |
annotate
|
2008-03-29 |
wenzelm |
* Eliminated destructive theorem database.
|
file |
diff |
annotate
|
2008-03-27 |
haftmann |
explicit case names for rule list_induct2
|
file |
diff |
annotate
|
2008-03-27 |
wenzelm |
Command 'setup': discontinued implicit version.
|
file |
diff |
annotate
|
2008-03-27 |
wenzelm |
HOL (and FOL): renamed variables in rules imp_elim and swap;
|
file |
diff |
annotate
|
2008-03-25 |
wenzelm |
Functor NamedThmsFun: data is available to the user as dynamic fact;
|
file |
diff |
annotate
|
2008-03-24 |
wenzelm |
removed obsolete use_legacy_bindings;
|
file |
diff |
annotate
|
2008-03-20 |
haftmann |
Theory Product_Type; fixed typos
|
file |
diff |
annotate
|
2008-03-19 |
wenzelm |
removed redundant Nat.less_not_sym, Nat.less_asym;
|
file |
diff |
annotate
|
2008-03-19 |
paulson |
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
|
file |
diff |
annotate
|
2008-03-18 |
wenzelm |
theory loader: discontinued *attached* ML scripts;
|
file |
diff |
annotate
|