| 2003-06-26 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-06-26 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-06-26 |
paulson |
Conversion of "Merge" to Isar format
|
changeset |
files
|
| 2003-06-25 |
paulson |
Conversion of UNITY/Distributor to Isar script. General tidy-up.
|
changeset |
files
|
| 2003-06-24 |
paulson |
Converting ZF/UNITY to Isar
|
changeset |
files
|
| 2003-06-24 |
berghofe |
Added new theories StrongNorm and WeakNorm to Lambda example.
|
changeset |
files
|
| 2003-06-24 |
berghofe |
Bibliography file with paper by Matthes and Joachimski.
|
changeset |
files
|
| 2003-06-24 |
berghofe |
Added bibliography.
|
changeset |
files
|
| 2003-06-24 |
berghofe |
Added new theories WeakNorm and StrongNorm.
|
changeset |
files
|
| 2003-06-24 |
berghofe |
Added lift_map and subst_map.
|
changeset |
files
|
| 2003-06-24 |
berghofe |
Nicer syntax for beta reduction.
|
changeset |
files
|
| 2003-06-24 |
berghofe |
Moved strong normalization proof to StrongNorm.thy
|
changeset |
files
|
| 2003-06-24 |
berghofe |
New proof of weak normalization with program extraction.
|
changeset |
files
|
| 2003-06-21 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-06-20 |
paulson |
conversion of ClientImpl to Isar script
|
changeset |
files
|
| 2003-06-20 |
paulson |
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
|
changeset |
files
|
| 2003-06-19 |
paulson |
inserted TUM in other places
|
changeset |
files
|
| 2003-06-16 |
paulson |
added TUM
|
changeset |
files
|
| 2003-06-12 |
paulson |
x-symbols (mostly)
|
changeset |
files
|
| 2003-06-02 |
kleing |
remove -p option, separate setting available
|
changeset |
files
|
| 2003-06-02 |
paulson |
Further tweaks of ZF/UNITY
|
changeset |
files
|
| 2003-05-30 |
paulson |
getting ZF/UNITY working again
|
changeset |
files
|
| 2003-05-29 |
paulson |
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
|
changeset |
files
|
| 2003-05-28 |
paulson |
some new ZF/UNITY material from Sidi Ehmety
|
changeset |
files
|
| 2003-05-28 |
paulson |
examples now use Complex_Main
|
changeset |
files
|
| 2003-05-28 |
paulson |
new theorem
|
changeset |
files
|
| 2003-05-27 |
berghofe |
Added term_of function for product type.
|
changeset |
files
|
| 2003-05-27 |
berghofe |
Added pair_const.
|
changeset |
files
|
| 2003-05-27 |
paulson |
removed redundant line
|
changeset |
files
|
| 2003-05-27 |
paulson |
updating ZF-UNITY with Sidi's new material
|
changeset |
files
|
| 2003-05-26 |
streckem |
Introduced distinction wf_prog vs. ws_prog
|
changeset |
files
|
| 2003-05-26 |
kleing |
set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible)
|
changeset |
files
|
| 2003-05-24 |
kleing |
fixed
|
changeset |
files
|
| 2003-05-23 |
kleing |
make it possible to switch off proof objects for HOL image
|
changeset |
files
|
| 2003-05-23 |
kleing |
make it possible to switch off proof objects
|
changeset |
files
|
| 2003-05-20 |
kleing |
be less verbose about simplification depth
|
changeset |
files
|
| 2003-05-18 |
kleing |
fix typo
|
changeset |
files
|
| 2003-05-18 |
kleing |
attach log files
|
changeset |
files
|
| 2003-05-18 |
kleing |
more cleanup
|
changeset |
files
|
| 2003-05-18 |
kleing |
fix mime stuff
|
changeset |
files
|
| 2003-05-18 |
kleing |
attach log files
|
changeset |
files
|
| 2003-05-18 |
kleing |
support text file attachments
|
changeset |
files
|
| 2003-05-16 |
webertj |
Added a few lemmas about map_le
|
changeset |
files
|
| 2003-05-15 |
kleing |
give tests time to copy settings
|
changeset |
files
|
| 2003-05-14 |
schirmer |
Added Bali to test
|
changeset |
files
|
| 2003-05-14 |
schirmer |
Adapted to changes in Map.thy
|
changeset |
files
|
| 2003-05-14 |
kleing |
use proof objects for HOL by default
|
changeset |
files
|
| 2003-05-14 |
nipkow |
eparation logic - a beginning.
|
changeset |
files
|
| 2003-05-14 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-05-14 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-05-14 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-05-13 |
kleing |
HOL-Real -> HOL-Complex
Isabelle2003
|
changeset |
files
|
| 2003-05-12 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-05-12 |
paulson |
tweaked
|
changeset |
files
|
| 2003-05-12 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2003-05-12 |
paulson |
oops
|
changeset |
files
|
| 2003-05-12 |
kleing |
different colors for new release
|
changeset |
files
|
| 2003-05-12 |
ballarin |
Improved entry on Algebra.
|
changeset |
files
|
| 2003-05-12 |
kleing |
no separate x-symbol package
|
changeset |
files
|
| 2003-05-12 |
kleing |
Isabelle2002
|
changeset |
files
|