| Sun, 18 May 2003 16:15:01 +0200 |
kleing |
fix mime stuff
|
changeset |
files
|
| Sun, 18 May 2003 15:28:41 +0200 |
kleing |
attach log files
|
changeset |
files
|
| Sun, 18 May 2003 15:15:13 +0200 |
kleing |
support text file attachments
|
changeset |
files
|
| Fri, 16 May 2003 16:35:36 +0200 |
webertj |
Added a few lemmas about map_le
|
changeset |
files
|
| Thu, 15 May 2003 11:22:54 +0200 |
kleing |
give tests time to copy settings
|
changeset |
files
|
| Wed, 14 May 2003 20:36:29 +0200 |
schirmer |
Added Bali to test
|
changeset |
files
|
| Wed, 14 May 2003 20:29:18 +0200 |
schirmer |
Adapted to changes in Map.thy
|
changeset |
files
|
| Wed, 14 May 2003 15:22:37 +0200 |
kleing |
use proof objects for HOL by default
|
changeset |
files
|
| Wed, 14 May 2003 14:20:55 +0200 |
nipkow |
eparation logic - a beginning.
|
changeset |
files
|
| Wed, 14 May 2003 11:15:18 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 14 May 2003 10:33:52 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 14 May 2003 10:22:09 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 13 May 2003 08:59:21 +0200 |
kleing |
HOL-Real -> HOL-Complex
Isabelle2003
|
changeset |
files
|
| Mon, 12 May 2003 19:54:43 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 12 May 2003 18:50:07 +0200 |
paulson |
tweaked
|
changeset |
files
|
| Mon, 12 May 2003 18:42:21 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 12 May 2003 18:11:44 +0200 |
paulson |
oops
|
changeset |
files
|
| Mon, 12 May 2003 15:57:46 +0200 |
kleing |
different colors for new release
|
changeset |
files
|
| Mon, 12 May 2003 15:51:34 +0200 |
ballarin |
Improved entry on Algebra.
|
changeset |
files
|
| Mon, 12 May 2003 15:49:37 +0200 |
kleing |
no separate x-symbol package
|
changeset |
files
|
| Mon, 12 May 2003 15:46:35 +0200 |
kleing |
Isabelle2002
|
changeset |
files
|
| Mon, 12 May 2003 15:46:13 +0200 |
kleing |
removed new jersey mirror
|
changeset |
files
|
| Mon, 12 May 2003 15:07:11 +0200 |
kleing |
done
|
changeset |
files
|
| Mon, 12 May 2003 15:06:43 +0200 |
kleing |
moved % comments out of ttboxes
|
changeset |
files
|
| Mon, 12 May 2003 14:49:08 +0200 |
kleing |
be nice on sunbroy2
|
changeset |
files
|
| Mon, 12 May 2003 14:17:55 +0200 |
kleing |
MicroJava LBV
|
changeset |
files
|
| Mon, 12 May 2003 14:16:38 +0200 |
schirmer |
Bali
|
changeset |
files
|
| Mon, 12 May 2003 13:57:23 +0200 |
kleing |
removed references to KDE versions (works for any).
|
changeset |
files
|
| Mon, 12 May 2003 13:51:50 +0200 |
berghofe |
Program extraction framework.
|
changeset |
files
|
| Mon, 12 May 2003 13:49:08 +0200 |
kleing |
smlnj link update, x-symbol/PG update
|
changeset |
files
|
| Mon, 12 May 2003 12:36:22 +0200 |
paulson |
some information for Constructible
|
changeset |
files
|
| Mon, 12 May 2003 12:27:10 +0200 |
paulson |
some information for Complex
|
changeset |
files
|
| Mon, 12 May 2003 12:26:50 +0200 |
paulson |
updated text
|
changeset |
files
|
| Mon, 12 May 2003 12:12:19 +0200 |
kleing |
makefiles for latex runs
|
changeset |
files
|
| Mon, 12 May 2003 11:56:29 +0200 |
kleing |
defer latex run to Makefile (not IsaMakefile)
|
changeset |
files
|
| Mon, 12 May 2003 11:54:29 +0200 |
kleing |
added isar-overview
|
changeset |
files
|
| Mon, 12 May 2003 11:34:49 +0200 |
kleing |
added IsarOverview
|
changeset |
files
|
| Mon, 12 May 2003 11:33:55 +0200 |
kleing |
IsarOverview moved one level up
|
changeset |
files
|
| Sat, 10 May 2003 20:53:02 +0200 |
berghofe |
Added new function eta_long.
|
changeset |
files
|
| Sat, 10 May 2003 20:52:18 +0200 |
berghofe |
- Added split_min and split_max to preprocessor
|
changeset |
files
|
| Fri, 09 May 2003 18:00:30 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 09 May 2003 17:19:58 +0200 |
ballarin |
NEWS updated for HOL-Algebra.
|
changeset |
files
|
| Fri, 09 May 2003 14:21:07 +0200 |
kleing |
tuned
|
changeset |
files
|
| Fri, 09 May 2003 14:15:50 +0200 |
kleing |
only make development snapshots for successful tests
|
changeset |
files
|
| Fri, 09 May 2003 14:08:04 +0200 |
kleing |
fixes
|
changeset |
files
|
| Fri, 09 May 2003 12:08:00 +0200 |
kleing |
var/run -> var/running
|
changeset |
files
|
| Fri, 09 May 2003 12:02:57 +0200 |
kleing |
tuned
|
changeset |
files
|
| Fri, 09 May 2003 11:56:16 +0200 |
kleing |
typo
|
changeset |
files
|
| Fri, 09 May 2003 11:54:33 +0200 |
kleing |
add cleanup of old error log and test-still-running files
|
changeset |
files
|
| Fri, 09 May 2003 11:54:04 +0200 |
kleing |
tuned
|
changeset |
files
|
| Fri, 09 May 2003 11:47:29 +0200 |
kleing |
check for error log, send mail if exists
|
changeset |
files
|
| Fri, 09 May 2003 11:26:17 +0200 |
kleing |
leave error messages in error.log, send only one email for all platforms
|
changeset |
files
|
| Thu, 08 May 2003 17:44:38 +0200 |
paulson |
new theory Complex_Main as basis for analysis developments
|
changeset |
files
|
| Thu, 08 May 2003 15:23:21 +0200 |
paulson |
now refers to Complex and Complex_Main
|
changeset |
files
|
| Thu, 08 May 2003 13:37:51 +0200 |
kleing |
-> HOL-Complex-HahnBanach in clean target
|
changeset |
files
|
| Thu, 08 May 2003 13:36:07 +0200 |
kleing |
fix euro error
|
changeset |
files
|
| Thu, 08 May 2003 13:10:02 +0200 |
paulson |
removed obsolete references to HOL-Real
|
changeset |
files
|
| Thu, 08 May 2003 12:52:15 +0200 |
paulson |
HOL-Complex
|
changeset |
files
|
| Thu, 08 May 2003 12:51:55 +0200 |
paulson |
auto update
|
changeset |
files
|
| Thu, 08 May 2003 12:50:27 +0200 |
paulson |
HOL-Real -> HOL-Complex
|
changeset |
files
|
| Thu, 08 May 2003 10:35:24 +0200 |
paulson |
new version copied here
|
changeset |
files
|
| Wed, 07 May 2003 22:07:33 +0200 |
ballarin |
Small changes for release Isabelle 2003.
|
changeset |
files
|
| Wed, 07 May 2003 17:46:04 +0200 |
kleing |
use different main class for batch mode
|
changeset |
files
|
| Wed, 07 May 2003 17:41:23 +0200 |
kleing |
fixed javac warning
|
changeset |
files
|
| Wed, 07 May 2003 17:40:48 +0200 |
kleing |
fixed uncollapsed dirs (should be collapsed by default)
|
changeset |
files
|
| Wed, 07 May 2003 17:06:11 +0200 |
kleing |
target clean, compile Console.java
|
changeset |
files
|
| Wed, 07 May 2003 17:04:45 +0200 |
kleing |
cleanup, comments
|
changeset |
files
|
| Wed, 07 May 2003 16:58:17 +0200 |
berghofe |
Some tuning:
|
changeset |
files
|
| Wed, 07 May 2003 16:38:55 +0200 |
kleing |
eliminated dependencies on AWT for batch mode
|
changeset |
files
|
| Wed, 07 May 2003 14:53:35 +0200 |
kleing |
fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach)
|
changeset |
files
|
| Tue, 06 May 2003 17:45:54 +0200 |
paulson |
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
|
changeset |
files
|
| Tue, 06 May 2003 12:29:49 +0200 |
kleing |
use -Smax with poly 4.1.3 for maximum database space (see poly release notes)
|
changeset |
files
|
| Tue, 06 May 2003 10:47:17 +0200 |
kleing |
fixed missing -g true for HOL-Auth
|
changeset |
files
|
| Tue, 06 May 2003 10:40:43 +0200 |
paulson |
new version
|
changeset |
files
|
| Tue, 06 May 2003 09:23:13 +0200 |
kleing |
use /usr/stud/isatest as home for all platforms (macbroy33 has no /home/stud/..)
|
changeset |
files
|
| Mon, 05 May 2003 18:36:00 +0200 |
paulson |
new directory Complex
|
changeset |
files
|
| Mon, 05 May 2003 18:34:16 +0200 |
paulson |
Complex, etc
|
changeset |
files
|
| Mon, 05 May 2003 18:30:48 +0200 |
paulson |
deleted obsolete group formalization
|
changeset |
files
|
| Mon, 05 May 2003 18:23:40 +0200 |
paulson |
New material on integration, etc. Moving Hyperreal/ex
|
changeset |
files
|
| Mon, 05 May 2003 18:22:31 +0200 |
paulson |
new session Complex for the complex numbers
|
changeset |
files
|
| Mon, 05 May 2003 18:22:01 +0200 |
paulson |
improved presentation of HOL/Auth theories
|
changeset |
files
|
| Mon, 05 May 2003 15:55:56 +0200 |
kleing |
add mac test
|
changeset |
files
|
| Mon, 05 May 2003 13:52:19 +0200 |
kleing |
fixed \<0>..\<9> (-> \<zero>..\<nine>)
|
changeset |
files
|
| Mon, 05 May 2003 13:42:16 +0200 |
kleing |
document preparation tuning
|
changeset |
files
|
| Mon, 05 May 2003 10:53:27 +0200 |
ballarin |
Fixed but with old versions of pdflatex (fancy symbols not allowed in bookmarks).
|
changeset |
files
|
| Sat, 03 May 2003 13:31:07 +0200 |
kleing |
fix for new \isasymeuro
|
changeset |
files
|
| Fri, 02 May 2003 20:06:59 +0200 |
ballarin |
File for document preparation.
|
changeset |
files
|
| Fri, 02 May 2003 20:02:50 +0200 |
ballarin |
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
|
changeset |
files
|
| Fri, 02 May 2003 16:43:36 +0200 |
kleing |
reduced package dependencies,
|
changeset |
files
|
| Fri, 02 May 2003 16:39:38 +0200 |
kleing |
removed package marvosym (breaks \Rightarrow)
|
changeset |
files
|
| Fri, 02 May 2003 15:19:36 +0200 |
kleing |
more documentation for packages in root.tex
|
changeset |
files
|
| Fri, 02 May 2003 10:25:42 +0200 |
paulson |
moved Bij.thy from HOL/GroupTheory
|
changeset |
files
|
| Thu, 01 May 2003 11:54:18 +0200 |
paulson |
new proofs about direct products, etc.
|
changeset |
files
|
| Thu, 01 May 2003 10:29:44 +0200 |
paulson |
moving Bij.thy from GroupTheory to Algebra
|
changeset |
files
|
| Thu, 01 May 2003 08:39:37 +0200 |
berghofe |
induct_impliesI is now unfolded.
|
changeset |
files
|
| Wed, 30 Apr 2003 18:33:41 +0200 |
ballarin |
Unknown change.
|
changeset |
files
|
| Wed, 30 Apr 2003 18:32:06 +0200 |
ballarin |
HOL-Algebra: New polynomial development added.
|
changeset |
files
|
| Wed, 30 Apr 2003 18:31:38 +0200 |
ballarin |
HOL-Algebra: new dependencies.
|
changeset |
files
|
| Wed, 30 Apr 2003 18:30:57 +0200 |
ballarin |
Simplifier: congruence rule update.
|
changeset |
files
|
| Wed, 30 Apr 2003 17:53:47 +0200 |
nipkow |
added a thm
|
changeset |
files
|
| Wed, 30 Apr 2003 10:01:35 +0200 |
ballarin |
Greatly extended CRing. Added Module.
|
changeset |
files
|
| Tue, 29 Apr 2003 12:36:49 +0200 |
paulson |
tweaks
|
changeset |
files
|
| Tue, 29 Apr 2003 12:36:40 +0200 |
paulson |
better guarantees
|
changeset |
files
|
| Mon, 28 Apr 2003 17:52:52 +0200 |
kleing |
in \isanewline: \\ -> \par
|
changeset |
files
|
| Mon, 28 Apr 2003 12:01:45 +0200 |
ballarin |
Simplifier no longer aborts on failed congruence proof.
|
changeset |
files
|
| Mon, 28 Apr 2003 10:33:57 +0200 |
berghofe |
Converted main proof to Isar.
|
changeset |
files
|
| Mon, 28 Apr 2003 10:33:42 +0200 |
berghofe |
Converted main proofs to Isar.
|
changeset |
files
|
| Mon, 28 Apr 2003 09:58:12 +0200 |
berghofe |
Added "break" flag to allow line breaks within \isa{...}
|
changeset |
files
|
| Sun, 27 Apr 2003 22:53:11 +0200 |
berghofe |
Fixed problem in add_elim_realizer (concerning inductive predicates with
|
changeset |
files
|
| Sat, 26 Apr 2003 12:44:29 +0200 |
paulson |
converting more HOL-Auth to new-style theories
|
changeset |
files
|
| Sat, 26 Apr 2003 12:38:42 +0200 |
paulson |
converting more HOL-Auth to new-style theories
|
changeset |
files
|
| Sat, 26 Apr 2003 12:38:17 +0200 |
paulson |
catches exception DELETE
|
changeset |
files
|
| Fri, 25 Apr 2003 15:17:36 +0200 |
kleing |
no need to be nice everywhere
|
changeset |
files
|
| Fri, 25 Apr 2003 11:18:41 +0200 |
paulson |
Auth: certified email protocol
|
changeset |
files
|
| Fri, 25 Apr 2003 11:18:14 +0200 |
paulson |
Changes required by the certified email protocol
|
changeset |
files
|
| Wed, 23 Apr 2003 18:09:48 +0200 |
berghofe |
Fixed problem in add_elim_realizer which caused bound variables to
|
changeset |
files
|
| Wed, 23 Apr 2003 13:33:55 +0200 |
kleing |
more documentation
|
changeset |
files
|
| Wed, 23 Apr 2003 13:06:36 +0200 |
paulson |
Got rid of the [iff], which was effectively inserting converseD
|
changeset |
files
|
| Wed, 23 Apr 2003 00:14:55 +0200 |
berghofe |
Tuned realizer for exE rule, to avoid blowup of extracted program.
|
changeset |
files
|
| Wed, 23 Apr 2003 00:13:32 +0200 |
berghofe |
elim_vars now handles both Vars and Frees.
|
changeset |
files
|