| 2000-04-17 |
wenzelm |
* improved name spaces: ambiguous output is qualified; support for
|
file |
diff |
annotate
|
| 2000-04-13 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2000-04-05 |
wenzelm |
Isar: simplified (more robust) goal selection of proof methods;
|
file |
diff |
annotate
|
| 2000-04-01 |
wenzelm |
recdef: admit name and atts;
|
file |
diff |
annotate
|
| 2000-03-30 |
nipkow |
recdef
|
file |
diff |
annotate
|
| 2000-03-30 |
wenzelm |
* Isar/Pure: local results and corresponding term bindings are now
|
file |
diff |
annotate
|
| 2000-03-29 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2000-03-24 |
wenzelm |
HOL/ex/Multiquote;
|
file |
diff |
annotate
|
| 2000-03-24 |
wenzelm |
usedir -D: update styles;
|
file |
diff |
annotate
|
| 2000-03-20 |
wenzelm |
improved support for emulating tactic scripts;
|
file |
diff |
annotate
|
| 2000-03-18 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2000-03-15 |
wenzelm |
Isar: splitter support; improved diagnostics;
|
file |
diff |
annotate
|
| 2000-03-13 |
wenzelm |
* HOL: exhaust_tac on datatypes superceded by new case_tac;
|
file |
diff |
annotate
|
| 2000-03-13 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2000-03-10 |
nipkow |
cases_tac
|
file |
diff |
annotate
|
| 2000-03-09 |
paulson |
Factorization
|
file |
diff |
annotate
|
| 2000-03-08 |
wenzelm |
* isatool mkdir provides easy setup of Isabelle session directories,
|
file |
diff |
annotate
|
| 2000-02-22 |
wenzelm |
* Pure now provides its own version of intro/elim/dest attributes;
|
file |
diff |
annotate
|
| 2000-02-21 |
wenzelm |
HOL/record: fixed select-update simplification procedure to handle
|
file |
diff |
annotate
|
| 2000-02-07 |
wenzelm |
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
|
file |
diff |
annotate
|
| 2000-02-02 |
wenzelm |
nat as names;
|
file |
diff |
annotate
|
| 1999-11-12 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-11-11 |
paulson |
HOL changes
|
file |
diff |
annotate
|
| 1999-11-11 |
wenzelm |
header;
|
file |
diff |
annotate
|
| 1999-10-30 |
wenzelm |
Isabelle99;
|
file |
diff |
annotate
|
| 1999-10-22 |
wenzelm |
tuned simplifier trace output; new flag debug_simp
|
file |
diff |
annotate
|
| 1999-10-20 |
wenzelm |
the settings environment is now statically scoped;
|
file |
diff |
annotate
|
| 1999-10-14 |
wenzelm |
document preparation based on (PDF)LaTeX;
|
file |
diff |
annotate
|
| 1999-10-13 |
berghofe |
Eliminated mutual_induct_tac.
|
file |
diff |
annotate
|
| 1999-10-08 |
wenzelm |
theorem database now also indexes constants "Trueprop", "all",
|
file |
diff |
annotate
|
| 1999-10-08 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-10-07 |
berghofe |
Documented changes to HOL/inductive and function thm_deps.
|
file |
diff |
annotate
|
| 1999-10-04 |
wenzelm |
added BVC;
|
file |
diff |
annotate
|
| 1999-09-29 |
wenzelm |
proper handling of dangling sort hypotheses (at last!);
|
file |
diff |
annotate
|
| 1999-09-28 |
nipkow |
incompatibility solver
|
file |
diff |
annotate
|
| 1999-09-24 |
wenzelm |
* HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
|
file |
diff |
annotate
|
| 1999-09-24 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-09-06 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| 1999-09-03 |
wenzelm |
added bind_thms;
|
file |
diff |
annotate
|
| 1999-09-03 |
paulson |
new SVC url
|
file |
diff |
annotate
|
| 1999-09-01 |
wenzelm |
structures Vartab / Termtab (instances of TableFun);
|
file |
diff |
annotate
|
| 1999-08-23 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-08-23 |
wenzelm |
record_simproc;
|
file |
diff |
annotate
|
| 1999-08-23 |
nipkow |
simplifier flex heads.
|
file |
diff |
annotate
|
| 1999-08-23 |
berghofe |
Moved sum_case to theory HOL/Datatype.
|
file |
diff |
annotate
|
| 1999-08-21 |
wenzelm |
real numerals;
|
file |
diff |
annotate
|
| 1999-08-19 |
wenzelm |
* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
|
file |
diff |
annotate
|
| 1999-08-19 |
paulson |
defer_recdef
|
file |
diff |
annotate
|
| 1999-08-19 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-08-18 |
wenzelm |
sum_case renamed to basic_sum_case;
|
file |
diff |
annotate
|
| 1999-08-18 |
wenzelm |
replaced 'ProofGeneral' by 'Proof General';
|
file |
diff |
annotate
|
| 1999-08-17 |
wenzelm |
replaced HOL_quantifiers flag by "HOL" print mode;
|
file |
diff |
annotate
|
| 1999-08-16 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-08-16 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-08-11 |
nipkow |
Removed
|
file |
diff |
annotate
|
| 1999-08-09 |
wenzelm |
theory loader actions;
|
file |
diff |
annotate
|
| 1999-08-03 |
paulson |
SVC
|
file |
diff |
annotate
|
| 1999-07-28 |
wenzelm |
HOL-Real target now builds an actual image;
|
file |
diff |
annotate
|
| 1999-07-28 |
paulson |
LK
|
file |
diff |
annotate
|
| 1999-07-19 |
berghofe |
Datatype package now handles arbitrarily branching datatypes.
|
file |
diff |
annotate
|