2004-10-05 |
paulson |
auto update
|
changeset |
files
|
2004-10-05 |
paulson |
new simprules for abs and for things like a/b<1
|
changeset |
files
|
2004-10-04 |
paulson |
revised simprules for division
|
changeset |
files
|
2004-10-04 |
paulson |
PDF_VIEWER suggestion
|
changeset |
files
|
2004-10-04 |
paulson |
Abstract for the Isabelle system
|
changeset |
files
|
2004-10-02 |
aspinall |
Add openblock/closeblock to other opengoal/closegoal elements
|
changeset |
files
|
2004-10-01 |
aspinall |
Allow scanning to recover and reconstruct bad input
|
changeset |
files
|
2004-10-01 |
paulson |
patch to "display"
|
changeset |
files
|
2004-10-01 |
paulson |
display-drafts now uses pdf!
|
changeset |
files
|
2004-10-01 |
paulson |
tweaking of arithmetic proofs
|
changeset |
files
|
2004-10-01 |
aspinall |
Comments
|
changeset |
files
|
2004-09-30 |
paulson |
tidied
|
changeset |
files
|
2004-09-30 |
kleing |
display pdf as well as dvi
|
changeset |
files
|
2004-09-30 |
schirmer |
bug-fix with new records
|
changeset |
files
|
2004-09-29 |
aspinall |
Remove white space skipping in element content; XML specification clearly requires whitespace to be passed to application.
|
changeset |
files
|
2004-09-29 |
schirmer |
tuned performance of record definition
|
changeset |
files
|
2004-09-29 |
paulson |
tidying up; identifying the main theorems
|
changeset |
files
|
2004-09-28 |
ballarin |
Changes in "includes".
|
changeset |
files
|
2004-09-28 |
ballarin |
Bug fixes.
|
changeset |
files
|
2004-09-28 |
aspinall |
Add text_charref to encode a string using character references
|
changeset |
files
|
2004-09-28 |
aspinall |
Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
|
changeset |
files
|
2004-09-28 |
aspinall |
Fix to unparse to not double-escape backslash
|
changeset |
files
|
2004-09-27 |
aspinall |
Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
|
changeset |
files
|
2004-09-27 |
aspinall |
Add newline after CDATA for sake of HaXml
|
changeset |
files
|
2004-09-27 |
ballarin |
Modified locales: improved implementation of "includes".
|
changeset |
files
|
2004-09-23 |
paulson |
some x-symbols
|
changeset |
files
|
2004-09-23 |
berghofe |
- Inserted additional check for equality types in check_mode_clause that
|
changeset |
files
|
2004-09-22 |
schirmer |
bug-fix
|
changeset |
files
|
2004-09-19 |
paulson |
converting UNITY/MultisetSum.ML to Isar script
|
changeset |
files
|
2004-09-17 |
paulson |
converted ZF/Induct/Multiset to Isar script
|
changeset |
files
|
2004-09-13 |
nipkow |
*** empty log message ***
|
changeset |
files
|
2004-09-11 |
nipkow |
undoing previous change
|
changeset |
files
|
2004-09-11 |
nipkow |
antisymmetry simproc
|
changeset |
files
|
2004-09-10 |
nipkow |
Added antisymmetry simproc
|
changeset |
files
|
2004-09-10 |
obua |
IntInf.divMod replaced by IntInf.div, IntInt.mod
|
changeset |
files
|
2004-09-09 |
nipkow |
new forward deduction capability for simplifier
|
changeset |
files
|
2004-09-09 |
paulson |
new hooks for resolution by Jia Meng
|
changeset |
files
|
2004-09-08 |
aspinall |
Fix for schema changes in pgiptype
|
changeset |
files
|
2004-09-08 |
aspinall |
Tweak parentnames attribute on opentheory
|
changeset |
files
|
2004-09-08 |
aspinall |
Support parsing of -- {* comments *}. Add extra output channels.
|
changeset |
files
|
2004-09-08 |
aspinall |
Add info and debug output channels.
|
changeset |
files
|
2004-09-08 |
obua |
Adapted FloatArith.ML to SMLNJ 10.0.7
|
changeset |
files
|
2004-09-07 |
oheimb |
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
|
changeset |
files
|
2004-09-07 |
oheimb |
added check against indirect recursion
|
changeset |
files
|
2004-09-07 |
nipkow |
fixed discrete field.
|
changeset |
files
|
2004-09-07 |
nipkow |
tuned "discrete" field
|
changeset |
files
|
2004-09-06 |
nipkow |
made mult_mono_thms generic.
|
changeset |
files
|
2004-09-06 |
paulson |
now rejects degenerate (looping) cases
|
changeset |
files
|
2004-09-06 |
paulson |
new "respects" syntax for the congruent operator
|
changeset |
files
|
2004-09-03 |
nipkow |
*** empty log message ***
|
changeset |
files
|
2004-09-03 |
obua |
float2real is now globally available
|
changeset |
files
|
2004-09-03 |
obua |
Matrix theory
|
changeset |
files
|
2004-09-03 |
obua |
Matrix theory, linear programming
|
changeset |
files
|
2004-09-03 |
paulson |
new theorem symD
|
changeset |
files
|
2004-09-03 |
paulson |
listrel operator for lifting relations to lists
|
changeset |
files
|
2004-09-02 |
aspinall |
Fix file:/// and file://localhost/ to give absolute paths
|
changeset |
files
|
2004-09-02 |
aspinall |
Fix file:/// and file://localhost/ to return local file result
|
changeset |
files
|
2004-09-02 |
aspinall |
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
|
changeset |
files
|
2004-09-02 |
paulson |
new example of a quotiented nested data type
|
changeset |
files
|
2004-09-02 |
dixon |
added code to make use of case splitting to prove the specification equations for recursive definitions.
|
changeset |
files
|