2003-11-14 |
ballarin |
Type inference bug in Isar attributes "where" and "of" fixed.
|
file |
diff |
annotate
|
2003-11-06 |
schirmer |
Records:
|
file |
diff |
annotate
|
2003-11-06 |
ballarin |
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
|
file |
diff |
annotate
|
2003-10-22 |
paulson |
recursion
|
file |
diff |
annotate
|
2003-10-16 |
paulson |
line-breaks; rewording
|
file |
diff |
annotate
|
2003-10-15 |
kleing |
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
|
file |
diff |
annotate
|
2003-10-14 |
kleing |
allow \<^sub> in identifiers
|
file |
diff |
annotate
|
2003-10-09 |
skalberg |
Added info on the new 'finalconsts' command.
|
file |
diff |
annotate
|
2003-09-30 |
ballarin |
Improvements to Isar/Locales: premises generated by "includes" elements
|
file |
diff |
annotate
|
2003-09-23 |
paulson |
new session HOL-SET-Protocol
|
file |
diff |
annotate
|
2003-08-29 |
ballarin |
Method rule_tac understands Isar contexts: documentation.
|
file |
diff |
annotate
|
2003-08-29 |
skalberg |
Removed the extended digits again.
|
file |
diff |
annotate
|
2003-08-28 |
skalberg |
Fixed typos.
|
file |
diff |
annotate
|
2003-08-27 |
skalberg |
Extended the notion of letter and digit, such that now one may use greek,
|
file |
diff |
annotate
|
2003-07-29 |
kleing |
opened new section for next Isabelle release
|
file |
diff |
annotate
|
2003-07-21 |
skalberg |
Added the specification command.
|
file |
diff |
annotate
|
2003-05-12 |
ballarin |
Improved entry on Algebra.
|
file |
diff |
annotate
|
2003-05-12 |
kleing |
MicroJava LBV
|
file |
diff |
annotate
|
2003-05-12 |
schirmer |
Bali
|
file |
diff |
annotate
|
2003-05-12 |
berghofe |
Program extraction framework.
|
file |
diff |
annotate
|
2003-05-09 |
ballarin |
NEWS updated for HOL-Algebra.
|
file |
diff |
annotate
|
2003-05-06 |
paulson |
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
|
file |
diff |
annotate
|
2003-05-05 |
paulson |
Complex, etc
|
file |
diff |
annotate
|
2003-05-05 |
kleing |
fixed \<0>..\<9> (-> \<zero>..\<nine>)
|
file |
diff |
annotate
|
2003-05-05 |
kleing |
document preparation tuning
|
file |
diff |
annotate
|
2003-04-30 |
ballarin |
Simplifier: congruence rule update.
|
file |
diff |
annotate
|
2003-04-06 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2003-03-25 |
berghofe |
Presburger arithmetic
|
file |
diff |
annotate
|
2003-03-20 |
paulson |
Gauss, UNITY, ZF
|
file |
diff |
annotate
|
2003-03-18 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2003-02-27 |
ballarin |
Change to meta simplifier: congruence rules may now have frees as head of term.
|
file |
diff |
annotate
|
2003-02-25 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2003-02-20 |
paulson |
minor updates to pre-2002 release
|
file |
diff |
annotate
|
2003-02-11 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2003-01-17 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2002-12-11 |
ballarin |
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
|
file |
diff |
annotate
|
2002-11-28 |
ballarin |
HOL-Algebra partially ported to Isar.
|
file |
diff |
annotate
|
2002-10-14 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2002-10-10 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2002-10-10 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2002-10-01 |
berghofe |
Added some comments on new simplifier.
|
file |
diff |
annotate
|
2002-09-30 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2002-09-26 |
paulson |
GroupTheory and FuncSet
|
file |
diff |
annotate
|
2002-09-19 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2002-08-30 |
paulson |
removal of blast.overloaded
|
file |
diff |
annotate
|
2002-08-29 |
wenzelm |
updated;
|
file |
diff |
annotate
|
2002-08-27 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
2002-08-27 |
wenzelm |
* Pure: disallow duplicate fact bindings within new-style theory files;
|
file |
diff |
annotate
|
2002-08-27 |
wenzelm |
* Isar: preview of problems to finish 'show' now produce an error
|
file |
diff |
annotate
|
2002-08-23 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2002-08-13 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2002-08-12 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2002-08-08 |
wenzelm |
* Pure: improved error reporting of simprocs;
|
file |
diff |
annotate
|
2002-08-06 |
wenzelm |
* Provers: Simplifier.simproc(_i) now provide sane interface for
|
file |
diff |
annotate
|
2002-08-06 |
wenzelm |
* Pure: predefined locales "var" and "struct" are useful for sharing
|
file |
diff |
annotate
|
2002-08-02 |
wenzelm |
typedef: "open" option;
|
file |
diff |
annotate
|
2002-07-26 |
wenzelm |
support for split assumptions in cases (hyps vs. prems);
|
file |
diff |
annotate
|
2002-07-23 |
wenzelm |
* Pure: locale specifications now produce predicate definitions;
|
file |
diff |
annotate
|
2002-07-11 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2002-07-02 |
wenzelm |
thms_containing: optional limit argument;
|
file |
diff |
annotate
|