| 2001-10-25 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-10-25 |
wenzelm |
* HOL/record:
|
file |
diff |
annotate
|
| 2001-10-24 |
wenzelm |
* clasimp: ``iff'' declarations now handle conditional rules as well;
|
file |
diff |
annotate
|
| 2001-10-23 |
wenzelm |
* Pure: removed obsolete 'exported' attribute;
|
file |
diff |
annotate
|
| 2001-10-21 |
wenzelm |
* proper spacing of consecutive markup elements, especially text
|
file |
diff |
annotate
|
| 2001-10-20 |
wenzelm |
* greatly simplified document preparation setup, including more
|
file |
diff |
annotate
|
| 2001-10-17 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-10-16 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-10-16 |
wenzelm |
* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
|
file |
diff |
annotate
|
| 2001-10-15 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-10-15 |
wenzelm |
improved induct;
|
file |
diff |
annotate
|
| 2001-10-15 |
kleing |
canonical 'cases'/'induct' rules for n-tuples (n=3..7)
|
file |
diff |
annotate
|
| 2001-10-13 |
wenzelm |
* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
|
file |
diff |
annotate
|
| 2001-10-13 |
wenzelm |
* Pure: added 'corollary' command;
|
file |
diff |
annotate
|
| 2001-10-11 |
wenzelm |
* Isar/Pure: fixed 'token_translation' command;
|
file |
diff |
annotate
|
| 2001-10-08 |
wenzelm |
* added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;
|
file |
diff |
annotate
|
| 2001-10-05 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-10-05 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-10-04 |
wenzelm |
improved proof by cases and induction;
|
file |
diff |
annotate
|
| 2001-10-04 |
wenzelm |
* moved induct/cases attributes to Pure, added 'print_induct_rules' command;
|
file |
diff |
annotate
|
| 2001-10-03 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-09-28 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-09-27 |
wenzelm |
HOL: eliminated global items;
|
file |
diff |
annotate
|
| 2001-09-26 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-09-08 |
wenzelm |
* system: support Poly/ML 4.1.1 (large heaps);
|
file |
diff |
annotate
|
| 2001-09-04 |
wenzelm |
renamed "antecedent" case to "rule_context";
|
file |
diff |
annotate
|
| 2001-08-31 |
wenzelm |
* Proof General keywords specification is now part of the Isabelle
|
file |
diff |
annotate
|
| 2001-08-09 |
oheimb |
renamed addaltern to addafter, addSaltern to addSafter
|
file |
diff |
annotate
|
| 2001-08-08 |
wenzelm |
* HOL: syntax translations now work properly with numerals and records
|
file |
diff |
annotate
|
| 2001-08-07 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-08-07 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-07-20 |
wenzelm |
HOL: added "The";
|
file |
diff |
annotate
|
| 2001-07-03 |
paulson |
GroupTheory
|
file |
diff |
annotate
|
| 2001-06-05 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-05-21 |
paulson |
ZF: division
|
file |
diff |
annotate
|
| 2001-05-18 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-04-09 |
paulson |
Isar hint
|
file |
diff |
annotate
|
| 2001-02-23 |
oheimb |
renamed addaltern to addafter, addSaltern to addSafter
|
file |
diff |
annotate
|
| 2001-02-21 |
oheimb |
added split_conv_tac (also to claset()) as an optimization
|
file |
diff |
annotate
|
| 2001-02-20 |
oheimb |
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
|
file |
diff |
annotate
|
| 2001-02-15 |
oheimb |
added missiong word
|
file |
diff |
annotate
|
| 2001-02-14 |
wenzelm |
isatool install handles KDE version 1 or 2;
|
file |
diff |
annotate
|
| 2001-02-13 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-02-11 |
wenzelm |
more robust selection of calculational rules;
|
file |
diff |
annotate
|
| 2001-02-11 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-02-10 |
ballarin |
Updates to HOL/Algebra:
|
file |
diff |
annotate
|
| 2001-02-05 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-02-04 |
wenzelm |
* no_document ML operator temporarily disables LaTeX document
|
file |
diff |
annotate
|
| 2001-02-03 |
wenzelm |
HOL: inductive package no longer splits induction rule aggressively,
|
file |
diff |
annotate
|
| 2001-02-01 |
wenzelm |
* Pure: 'thms_containing' now takes actual terms as arguments;
|
file |
diff |
annotate
|
| 2001-01-30 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-01-24 |
wenzelm |
* Document preparation: renamed standard symbols \<ll> to \<lless> and
|
file |
diff |
annotate
|
| 2001-01-23 |
wenzelm |
added HOL-Unix example;
|
file |
diff |
annotate
|
| 2001-01-19 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-01-15 |
wenzelm |
* HOL/datatype: induction rule for arbitrarily branching datatypes is
|
file |
diff |
annotate
|
| 2001-01-11 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-01-10 |
wenzelm |
isatool unsymbolize;
|
file |
diff |
annotate
|
| 2001-01-10 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-01-10 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-01-06 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-01-05 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-01-03 |
wenzelm |
* Isar/HOL: added 'recdef_tc' command;
|
file |
diff |
annotate
|
| 2001-01-01 |
paulson |
Hyperreal
|
file |
diff |
annotate
|
| 2000-12-22 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2000-12-13 |
wenzelm |
* print modes "brackets" and "no_brackets" control output of nested =>
|
file |
diff |
annotate
|
| 2000-12-07 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2000-12-06 |
bauerg |
HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
|
file |
diff |
annotate
|
| 2000-11-30 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2000-11-30 |
wenzelm |
misc;
|
file |
diff |
annotate
|
| 2000-11-23 |
wenzelm |
* HOL: syntax or "abs";
|
file |
diff |
annotate
|
| 2000-11-16 |
paulson |
CTT
|
file |
diff |
annotate
|
| 2000-11-13 |
nipkow |
Removed > and >=
|
file |
diff |
annotate
|
| 2000-11-10 |
wenzelm |
* added overloaded operations "inverse" and "divide" (infix "/");
|
file |
diff |
annotate
|
| 2000-11-10 |
nipkow |
> etc
|
file |
diff |
annotate
|
| 2000-11-08 |
nipkow |
subgoals
|
file |
diff |
annotate
|
| 2000-11-06 |
wenzelm |
* Isar/HOL: method 'induct' now handles non-atomic goals; as a
|
file |
diff |
annotate
|
| 2000-11-04 |
wenzelm |
misc stuff;
|
file |
diff |
annotate
|
| 2000-10-25 |
wenzelm |
added HOL/Library/List_Prefix;
|
file |
diff |
annotate
|
| 2000-10-24 |
wenzelm |
* support sub/super scripts (for single symbols only), input syntax is
|
file |
diff |
annotate
|
| 2000-10-23 |
wenzelm |
* HOL: default proof step now includes 'intro_classes';
|
file |
diff |
annotate
|
| 2000-10-23 |
paulson |
contrapos
|
file |
diff |
annotate
|
| 2000-10-18 |
wenzelm |
* HOL/Library: a collection of generic theories to be used together
|
file |
diff |
annotate
|
| 2000-10-16 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2000-10-06 |
wenzelm |
* HOL/IMPP: extension of IMP with local variables and mutually
|
file |
diff |
annotate
|
| 2000-10-05 |
wenzelm |
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
|
file |
diff |
annotate
|
| 2000-10-03 |
wenzelm |
removed "symbols" syntax for constant "override";
|
file |
diff |
annotate
|
| 2000-10-02 |
wenzelm |
improved t.weak_case_cong text;
|
file |
diff |
annotate
|
| 2000-09-28 |
wenzelm |
Isabelle99-1 (October 2000);
|
file |
diff |
annotate
|
| 2000-09-26 |
wenzelm |
HOL/MicroJava;
|
file |
diff |
annotate
|
| 2000-09-23 |
paulson |
renaming the inverse image operator in HOL
|
file |
diff |
annotate
|
| 2000-09-15 |
wenzelm |
cleaned up and prepared for Isabelle99-1;
|
file |
diff |
annotate
|
| 2000-09-15 |
wenzelm |
system: isatool installfonts may handle X-Symbol fonts as well;
|
file |
diff |
annotate
|
| 2000-09-15 |
paulson |
renamed the select rules
|
file |
diff |
annotate
|
| 2000-09-12 |
wenzelm |
renamed atts: rulify to rule_format, elimify to elim_format;
|
file |
diff |
annotate
|
| 2000-09-12 |
wenzelm |
replaced "delrule" by "rule del";
|
file |
diff |
annotate
|
| 2000-09-07 |
wenzelm |
HOL: qed_spec_mp now also removes bounded ALL;
|
file |
diff |
annotate
|
| 2000-09-06 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2000-09-05 |
paulson |
meson_tac
|
file |
diff |
annotate
|
| 2000-09-02 |
wenzelm |
* HOL/Lambda: converted into new-style theory and document;
|
file |
diff |
annotate
|
| 2000-08-30 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2000-08-30 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2000-08-30 |
wenzelm |
fixed name;
|
file |
diff |
annotate
|
| 2000-08-30 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2000-08-29 |
wenzelm |
* 'pr' command: optional argument for ProofContext.prems_limit;
|
file |
diff |
annotate
|
| 2000-08-28 |
wenzelm |
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
|
file |
diff |
annotate
|
| 2000-08-28 |
wenzelm |
* \isabellestyle{it} produces near math mode output;
|
file |
diff |
annotate
|
| 2000-08-18 |
paulson |
new example ZF/ex/NatSum
|
file |
diff |
annotate
|
| 2000-08-17 |
wenzelm |
Isar/Pure: renamed 'RS' attribute to 'THEN';
|
file |
diff |
annotate
|
| 2000-08-11 |
paulson |
ZF arith
|
file |
diff |
annotate
|
| 2000-08-07 |
paulson |
ZF arith
|
file |
diff |
annotate
|
| 2000-08-01 |
wenzelm |
* blast(_tac) now handles actual object-logic rules as assumptions;
|
file |
diff |
annotate
|
| 2000-07-28 |
nipkow |
* HOL/While
|
file |
diff |
annotate
|
| 2000-07-24 |
wenzelm |
* Isar/Provers: intro/elim/dest attributes: changed
|
file |
diff |
annotate
|
| 2000-07-21 |
oheimb |
strengthened force_tac by using new first_best_tac
|
file |
diff |
annotate
|
| 2000-07-19 |
paulson |
// change; also moved entry for AddIffs
|
file |
diff |
annotate
|
| 2000-07-18 |
wenzelm |
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
|
file |
diff |
annotate
|
| 2000-07-16 |
wenzelm |
* tuned AST representation of nested pairs, avoiding bogus output in
|
file |
diff |
annotate
|
| 2000-07-14 |
paulson |
AddIffs
|
file |
diff |
annotate
|
| 2000-07-13 |
wenzelm |
HOL: the disjoint sum is now "<+>" instead of "Plus";
|
file |
diff |
annotate
|
| 2000-07-12 |
wenzelm |
infix 'OF' is a version of 'MRS' with more appropriate argument order;
|
file |
diff |
annotate
|