| 2004-03-15 |
paulson |
more up-to-date error msg
|
changeset |
files
|
| 2004-03-12 |
webertj |
\<dots> replaced by ...
|
changeset |
files
|
| 2004-03-11 |
webertj |
refute
|
changeset |
files
|
| 2004-03-11 |
webertj |
Documentation updated
|
changeset |
files
|
| 2004-03-11 |
webertj |
Refute_Examples added/fixed
|
changeset |
files
|
| 2004-03-11 |
kleing |
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
|
changeset |
files
|
| 2004-03-10 |
webertj |
SML/NJ compatibility fixes
|
changeset |
files
|
| 2004-03-10 |
webertj |
added Refute_Examples.thy
|
changeset |
files
|
| 2004-03-10 |
webertj |
changed default values for refute
|
changeset |
files
|
| 2004-03-10 |
webertj |
*** empty log message ***
|
changeset |
files
|
| 2004-03-10 |
webertj |
support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps
|
changeset |
files
|
| 2004-03-10 |
webertj |
Updated examples
|
changeset |
files
|
| 2004-03-10 |
webertj |
*** empty log message ***
|
changeset |
files
|
| 2004-03-10 |
webertj |
Internal and external SAT solvers
|
changeset |
files
|
| 2004-03-10 |
webertj |
Formulas of propositional logic
|
changeset |
files
|
| 2004-03-10 |
webertj |
ZCHAFF_HOME variable added
|
changeset |
files
|
| 2004-03-10 |
paulson |
new thm
|
changeset |
files
|
| 2004-03-10 |
paulson |
strengthened the axclass claims
|
changeset |
files
|
| 2004-03-09 |
kleing |
suggest -p 1 proof object level for HOL
|
changeset |
files
|
| 2004-03-09 |
kleing |
include more explanation of variables
|
changeset |
files
|
| 2004-03-08 |
ballarin |
*** empty log message ***
|
changeset |
files
|
| 2004-03-08 |
ballarin |
Bug-fixes for transitivity reasoner.
|
changeset |
files
|
| 2004-03-08 |
ballarin |
Added documentation for transitivity solver setup.
|
changeset |
files
|
| 2004-03-08 |
paulson |
generic theorems about exponentials; general tidying up
|
changeset |
files
|
| 2004-03-08 |
paulson |
new theory of infinite sets
|
changeset |
files
|
| 2004-03-06 |
nipkow |
Lex: removed last ML files
|
changeset |
files
|
| 2004-03-06 |
nipkow |
Conversion ML -> Isar
|
changeset |
files
|
| 2004-03-05 |
paulson |
tweaked for times_ac1
|
changeset |
files
|
| 2004-03-05 |
paulson |
tweaks
|
changeset |
files
|
| 2004-03-05 |
paulson |
some new results
|
changeset |
files
|
| 2004-03-05 |
paulson |
some new results
|
changeset |
files
|
| 2004-03-05 |
paulson |
Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
|
changeset |
files
|
| 2004-03-05 |
paulson |
patch to NumberTheory problems caused by Parity
|
changeset |
files
|
| 2004-03-05 |
kleing |
do not remove heaps, used for afp test
|
changeset |
files
|
| 2004-03-04 |
nipkow |
Lex: ML -> thy
|
changeset |
files
|
| 2004-03-04 |
nipkow |
ML -> Isar
|
changeset |
files
|
| 2004-03-04 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
changeset |
files
|
| 2004-03-04 |
nipkow |
Removed ML files from Lex
|
changeset |
files
|
| 2004-03-04 |
nipkow |
Conversion of ML files to Isar.
|
changeset |
files
|
| 2004-03-03 |
schirmer |
added record_ex_sel_eq_simproc
|
changeset |
files
|
| 2004-03-02 |
paulson |
fixed bugs in the setup of arithmetic procedures
|
changeset |
files
|
| 2004-03-02 |
paulson |
converted Hyperreal/IntFloor to Isar script
|
changeset |
files
|
| 2004-03-02 |
kleing |
tuned. proofs still gruesome..
|
changeset |
files
|
| 2004-03-02 |
kleing |
converted MiniML to Isar
|
changeset |
files
|
| 2004-03-02 |
kleing |
converted to Isar
|
changeset |
files
|
| 2004-03-01 |
paulson |
new Ring_and_Field hierarchy, eliminating redundant axioms
|
changeset |
files
|
| 2004-03-01 |
paulson |
converted Hyperreal/HTranscendental to Isar script
|
changeset |
files
|
| 2004-03-01 |
kleing |
converted to Isar
|
changeset |
files
|
| 2004-03-01 |
kleing |
union/intersection over intervals
|
changeset |
files
|
| 2004-02-29 |
berghofe |
Added specific code generator for number_of.
|
changeset |
files
|
| 2004-02-26 |
paulson |
converted Hyperreal/Series to Isar script
|
changeset |
files
|
| 2004-02-26 |
paulson |
converted Hyperreal/NatStar to Isar script
|
changeset |
files
|
| 2004-02-26 |
nipkow |
corrected authors
|
changeset |
files
|
| 2004-02-25 |
paulson |
converted Hyperreal/HSeries to Isar script
|
changeset |
files
|
| 2004-02-25 |
berghofe |
find_tname now handles parameter renaming properly ("as they are printed").
|
changeset |
files
|
| 2004-02-24 |
paulson |
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
|
changeset |
files
|
| 2004-02-24 |
paulson |
converted NSCA to Isar script
|
changeset |
files
|
| 2004-02-23 |
paulson |
converted HOL/Complex/NSInduct to Isar script
|
changeset |
files
|
| 2004-02-23 |
paulson |
converted HOL/Complex/NSCA to Isar script
|
changeset |
files
|
| 2004-02-21 |
paulson |
conversion of Complex/CStar to Isar script
|
changeset |
files
|