| 2003-03-25 |
berghofe |
Added hook for presburger arithmetic decision procedure.
|
changeset |
files
|
| 2003-03-25 |
berghofe |
New decision procedure for Presburger arithmetic.
|
changeset |
files
|
| 2003-03-23 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-03-21 |
paulson |
More on progress sets
|
changeset |
files
|
| 2003-03-21 |
paulson |
quadratic reciprocity files
|
changeset |
files
|
| 2003-03-20 |
paulson |
Gauss, UNITY, ZF
|
changeset |
files
|
| 2003-03-20 |
paulson |
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
|
changeset |
files
|
| 2003-03-18 |
paulson |
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
|
changeset |
files
|
| 2003-03-18 |
nipkow |
toggled show_main_goal
|
changeset |
files
|
| 2003-03-18 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-03-17 |
nipkow |
just a few mods to a few thms
|
changeset |
files
|
| 2003-03-17 |
paulson |
More "progress set" material
|
changeset |
files
|
| 2003-03-17 |
paulson |
moved one proof, added another
|
changeset |
files
|
| 2003-03-14 |
ballarin |
Bugs fixed and operators finprod and finsum.
|
changeset |
files
|
| 2003-03-14 |
kleing |
more about list_all2
|
changeset |
files
|
| 2003-03-14 |
kleing |
fix for changes in HOL/Hoare/
|
changeset |
files
|
| 2003-03-14 |
paulson |
Proved the main lemma on progress sets
|
changeset |
files
|
| 2003-03-14 |
paulson |
new UN/INT simprules
|
changeset |
files
|
| 2003-03-13 |
berghofe |
split_name no longer uses Sign.string_of_typ to encode types, since
|
changeset |
files
|
| 2003-03-11 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-03-11 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-03-11 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-03-11 |
berghofe |
addsplits / delsplits no longer ignore type of constant.
|
changeset |
files
|
| 2003-03-10 |
ballarin |
First distributed version of Group and Ring theory.
|
changeset |
files
|
| 2003-03-10 |
paulson |
New theory ProgressSets. Definition of closure sets
|
changeset |
files
|
| 2003-03-10 |
paulson |
spelling
|
changeset |
files
|
| 2003-03-06 |
paulson |
new UNITY examples theory
|
changeset |
files
|
| 2003-03-06 |
paulson |
new logical equivalences
|
changeset |
files
|
| 2003-03-06 |
paulson |
new simprule for int (nat n)
|
changeset |
files
|
| 2003-03-06 |
kleing |
link to devel snapshot
|
changeset |
files
|
| 2003-03-06 |
kleing |
obsolete
|
changeset |
files
|
| 2003-03-05 |
paulson |
new examples theory
|
changeset |
files
|
| 2003-03-02 |
kleing |
get cvs to change modified time for session.tex
|
changeset |
files
|
| 2003-03-01 |
kleing |
typo
|
changeset |
files
|
| 2003-03-01 |
kleing |
added exercises
|
changeset |
files
|
| 2003-03-01 |
kleing |
added Exercises
|
changeset |
files
|
| 2003-03-01 |
kleing |
keep a copy of generated files in repository
|
changeset |
files
|
| 2003-03-01 |
kleing |
keep a copy of generated files in repository
|
changeset |
files
|
| 2003-02-28 |
isatest |
generate nightly devel snapshot
|
changeset |
files
|
| 2003-02-28 |
isatest |
case distinction on host for makefile flags
|
changeset |
files
|
| 2003-02-27 |
paulson |
Reorganized, moving many results about the integer dvd relation from IntPrimes
|
changeset |
files
|
| 2003-02-27 |
paulson |
restored some deleted lemmas
|
changeset |
files
|
| 2003-02-27 |
ballarin |
Change to meta simplifier: congruence rules may now have frees as head of term.
|
changeset |
files
|
| 2003-02-26 |
kleing |
== -> =
|
changeset |
files
|
| 2003-02-26 |
paulson |
zprime_def fixes by Jeremy Avigad
|
changeset |
files
|
| 2003-02-26 |
paulson |
completed proofs for programs consisting of a single assignment
|
changeset |
files
|
| 2003-02-26 |
paulson |
new lemma
|
changeset |
files
|
| 2003-02-26 |
paulson |
some x-symbols and some new lemmas
|
changeset |
files
|
| 2003-02-25 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-02-25 |
nipkow |
added simp_depth_limit
|
changeset |
files
|
| 2003-02-25 |
berghofe |
Documented prf / full_prf commands and antiquotations.
|
changeset |
files
|
| 2003-02-25 |
nipkow |
Undid eta change for UN/INT.
|
changeset |
files
|
| 2003-02-20 |
paulson |
new inverse image lemmas
|
changeset |
files
|
| 2003-02-20 |
paulson |
minor updates to pre-2002 release
|
changeset |
files
|
| 2003-02-19 |
paulson |
fixed anomalies in the installed classical rules
|
changeset |
files
|
| 2003-02-18 |
kleing |
check maxs in defensive machine
|
changeset |
files
|
| 2003-02-18 |
paulson |
new theory Transformers: Meier-Sanders non-interference theory
|
changeset |
files
|
| 2003-02-17 |
mehta |
Proof of the Schorr-Waite graph marking algorithm.
|
changeset |
files
|
| 2003-02-16 |
paulson |
minor revisions
|
changeset |
files
|
| 2003-02-16 |
paulson |
new theorem Compl_partition2
|
changeset |
files
|