paulson [Mon, 02 Jun 2003 11:17:52 +0200] rev 14055
Further tweaks of ZF/UNITY
paulson [Fri, 30 May 2003 11:44:29 +0200] rev 14054
getting ZF/UNITY working again
paulson [Thu, 29 May 2003 17:10:00 +0200] rev 14053
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson [Wed, 28 May 2003 18:13:41 +0200] rev 14052
some new ZF/UNITY material from Sidi Ehmety
paulson [Wed, 28 May 2003 10:48:20 +0200] rev 14051
examples now use Complex_Main
paulson [Wed, 28 May 2003 10:47:54 +0200] rev 14050
new theorem
berghofe [Tue, 27 May 2003 17:39:43 +0200] rev 14049
Added term_of function for product type.
berghofe [Tue, 27 May 2003 17:39:17 +0200] rev 14048
Added pair_const.
paulson [Tue, 27 May 2003 11:46:29 +0200] rev 14047
removed redundant line
paulson [Tue, 27 May 2003 11:39:03 +0200] rev 14046
updating ZF-UNITY with Sidi's new material
streckem [Mon, 26 May 2003 18:36:15 +0200] rev 14045
Introduced distinction wf_prog vs. ws_prog
kleing [Mon, 26 May 2003 11:42:41 +0200] rev 14044
set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible)
switched off by default
kleing [Sat, 24 May 2003 19:52:53 +0200] rev 14043
fixed
kleing [Fri, 23 May 2003 17:19:53 +0200] rev 14042
make it possible to switch off proof objects for HOL image
kleing [Fri, 23 May 2003 17:18:10 +0200] rev 14041
make it possible to switch off proof objects
kleing [Tue, 20 May 2003 11:52:42 +0200] rev 14040
be less verbose about simplification depth
kleing [Sun, 18 May 2003 16:30:20 +0200] rev 14039
fix typo
kleing [Sun, 18 May 2003 16:29:18 +0200] rev 14038
attach log files
kleing [Sun, 18 May 2003 16:16:58 +0200] rev 14037
more cleanup
kleing [Sun, 18 May 2003 16:15:01 +0200] rev 14036
fix mime stuff
kleing [Sun, 18 May 2003 15:28:41 +0200] rev 14035
attach log files
kleing [Sun, 18 May 2003 15:15:13 +0200] rev 14034
support text file attachments
webertj [Fri, 16 May 2003 16:35:36 +0200] rev 14033
Added a few lemmas about map_le
kleing [Thu, 15 May 2003 11:22:54 +0200] rev 14032
give tests time to copy settings
schirmer [Wed, 14 May 2003 20:36:29 +0200] rev 14031
Added Bali to test
schirmer [Wed, 14 May 2003 20:29:18 +0200] rev 14030
Adapted to changes in Map.thy
kleing [Wed, 14 May 2003 15:22:37 +0200] rev 14029
use proof objects for HOL by default
nipkow [Wed, 14 May 2003 14:20:55 +0200] rev 14028
eparation logic - a beginning.
nipkow [Wed, 14 May 2003 11:15:18 +0200] rev 14027
*** empty log message ***
nipkow [Wed, 14 May 2003 10:33:52 +0200] rev 14026
*** empty log message ***
nipkow [Wed, 14 May 2003 10:22:09 +0200] rev 14025
*** empty log message ***
kleing [Tue, 13 May 2003 08:59:21 +0200] rev 14024
HOL-Real -> HOL-Complex
nipkow [Mon, 12 May 2003 19:54:43 +0200] rev 14023
*** empty log message ***
paulson [Mon, 12 May 2003 18:50:07 +0200] rev 14022
tweaked
nipkow [Mon, 12 May 2003 18:42:21 +0200] rev 14021
*** empty log message ***
paulson [Mon, 12 May 2003 18:11:44 +0200] rev 14020
oops
kleing [Mon, 12 May 2003 15:57:46 +0200] rev 14019
different colors for new release
ballarin [Mon, 12 May 2003 15:51:34 +0200] rev 14018
Improved entry on Algebra.
kleing [Mon, 12 May 2003 15:49:37 +0200] rev 14017
no separate x-symbol package
kleing [Mon, 12 May 2003 15:46:35 +0200] rev 14016
Isabelle2002
kleing [Mon, 12 May 2003 15:46:13 +0200] rev 14015
removed new jersey mirror
kleing [Mon, 12 May 2003 15:07:11 +0200] rev 14014
done
kleing [Mon, 12 May 2003 15:06:43 +0200] rev 14013
moved % comments out of ttboxes
kleing [Mon, 12 May 2003 14:49:08 +0200] rev 14012
be nice on sunbroy2
kleing [Mon, 12 May 2003 14:17:55 +0200] rev 14011
MicroJava LBV
schirmer [Mon, 12 May 2003 14:16:38 +0200] rev 14010
Bali
kleing [Mon, 12 May 2003 13:57:23 +0200] rev 14009
removed references to KDE versions (works for any).
berghofe [Mon, 12 May 2003 13:51:50 +0200] rev 14008
Program extraction framework.
kleing [Mon, 12 May 2003 13:49:08 +0200] rev 14007
smlnj link update, x-symbol/PG update
paulson [Mon, 12 May 2003 12:36:22 +0200] rev 14006
some information for Constructible
paulson [Mon, 12 May 2003 12:27:10 +0200] rev 14005
some information for Complex
paulson [Mon, 12 May 2003 12:26:50 +0200] rev 14004
updated text
kleing [Mon, 12 May 2003 12:12:19 +0200] rev 14003
makefiles for latex runs
kleing [Mon, 12 May 2003 11:56:29 +0200] rev 14002
defer latex run to Makefile (not IsaMakefile)
kleing [Mon, 12 May 2003 11:54:29 +0200] rev 14001
added isar-overview
kleing [Mon, 12 May 2003 11:34:49 +0200] rev 14000
added IsarOverview
kleing [Mon, 12 May 2003 11:33:55 +0200] rev 13999
IsarOverview moved one level up
berghofe [Sat, 10 May 2003 20:53:02 +0200] rev 13998
Added new function eta_long.
berghofe [Sat, 10 May 2003 20:52:18 +0200] rev 13997
- Added split_min and split_max to preprocessor
- Moved eta_long to Pure/pattern.ML
nipkow [Fri, 09 May 2003 18:00:30 +0200] rev 13996
*** empty log message ***
ballarin [Fri, 09 May 2003 17:19:58 +0200] rev 13995
NEWS updated for HOL-Algebra.
kleing [Fri, 09 May 2003 14:21:07 +0200] rev 13994
tuned
kleing [Fri, 09 May 2003 14:15:50 +0200] rev 13993
only make development snapshots for successful tests
kleing [Fri, 09 May 2003 14:08:04 +0200] rev 13992
fixes
kleing [Fri, 09 May 2003 12:08:00 +0200] rev 13991
var/run -> var/running
kleing [Fri, 09 May 2003 12:02:57 +0200] rev 13990
tuned
kleing [Fri, 09 May 2003 11:56:16 +0200] rev 13989
typo
kleing [Fri, 09 May 2003 11:54:33 +0200] rev 13988
add cleanup of old error log and test-still-running files
kleing [Fri, 09 May 2003 11:54:04 +0200] rev 13987
tuned
kleing [Fri, 09 May 2003 11:47:29 +0200] rev 13986
check for error log, send mail if exists
kleing [Fri, 09 May 2003 11:26:17 +0200] rev 13985
leave error messages in error.log, send only one email for all platforms
paulson [Thu, 08 May 2003 17:44:38 +0200] rev 13984
new theory Complex_Main as basis for analysis developments
paulson [Thu, 08 May 2003 15:23:21 +0200] rev 13983
now refers to Complex and Complex_Main
kleing [Thu, 08 May 2003 13:37:51 +0200] rev 13982
-> HOL-Complex-HahnBanach in clean target
kleing [Thu, 08 May 2003 13:36:07 +0200] rev 13981
fix euro error
paulson [Thu, 08 May 2003 13:10:02 +0200] rev 13980
removed obsolete references to HOL-Real
paulson [Thu, 08 May 2003 12:52:15 +0200] rev 13979
HOL-Complex
paulson [Thu, 08 May 2003 12:51:55 +0200] rev 13978
auto update
paulson [Thu, 08 May 2003 12:50:27 +0200] rev 13977
HOL-Real -> HOL-Complex
paulson [Thu, 08 May 2003 10:35:24 +0200] rev 13976
new version copied here
ballarin [Wed, 07 May 2003 22:07:33 +0200] rev 13975
Small changes for release Isabelle 2003.
kleing [Wed, 07 May 2003 17:46:04 +0200] rev 13974
use different main class for batch mode
kleing [Wed, 07 May 2003 17:41:23 +0200] rev 13973
fixed javac warning
kleing [Wed, 07 May 2003 17:40:48 +0200] rev 13972
fixed uncollapsed dirs (should be collapsed by default)
kleing [Wed, 07 May 2003 17:06:11 +0200] rev 13971
target clean, compile Console.java
kleing [Wed, 07 May 2003 17:04:45 +0200] rev 13970
cleanup, comments
berghofe [Wed, 07 May 2003 16:58:17 +0200] rev 13969
Some tuning:
- Replaced y in definition of L predicate by more suggestive v
- Eliminated rule_format attribute from proofs of lemma2 ... lemma4
- Removed superfluous "+" in proof of prop2
kleing [Wed, 07 May 2003 16:38:55 +0200] rev 13968
eliminated dependencies on AWT for batch mode
kleing [Wed, 07 May 2003 14:53:35 +0200] rev 13967
fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach)
paulson [Tue, 06 May 2003 17:45:54 +0200] rev 13966
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
kleing [Tue, 06 May 2003 12:29:49 +0200] rev 13965
use -Smax with poly 4.1.3 for maximum database space (see poly release notes)
kleing [Tue, 06 May 2003 10:47:17 +0200] rev 13964
fixed missing -g true for HOL-Auth
paulson [Tue, 06 May 2003 10:40:43 +0200] rev 13963
new version
kleing [Tue, 06 May 2003 09:23:13 +0200] rev 13962
use /usr/stud/isatest as home for all platforms (macbroy33 has no /home/stud/..)
paulson [Mon, 05 May 2003 18:36:00 +0200] rev 13961
new directory Complex
paulson [Mon, 05 May 2003 18:34:16 +0200] rev 13960
Complex, etc
paulson [Mon, 05 May 2003 18:30:48 +0200] rev 13959
deleted obsolete group formalization
paulson [Mon, 05 May 2003 18:23:40 +0200] rev 13958
New material on integration, etc. Moving Hyperreal/ex
to directory Complex
paulson [Mon, 05 May 2003 18:22:31 +0200] rev 13957
new session Complex for the complex numbers
paulson [Mon, 05 May 2003 18:22:01 +0200] rev 13956
improved presentation of HOL/Auth theories
kleing [Mon, 05 May 2003 15:55:56 +0200] rev 13955
add mac test
kleing [Mon, 05 May 2003 13:52:19 +0200] rev 13954
fixed \<0>..\<9> (-> \<zero>..\<nine>)
kleing [Mon, 05 May 2003 13:42:16 +0200] rev 13953
document preparation tuning
ballarin [Mon, 05 May 2003 10:53:27 +0200] rev 13952
Fixed but with old versions of pdflatex (fancy symbols not allowed in bookmarks).
kleing [Sat, 03 May 2003 13:31:07 +0200] rev 13951
fix for new \isasymeuro
ballarin [Fri, 02 May 2003 20:06:59 +0200] rev 13950
File for document preparation.
ballarin [Fri, 02 May 2003 20:02:50 +0200] rev 13949
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
kleing [Fri, 02 May 2003 16:43:36 +0200] rev 13948
reduced package dependencies,
use babel standard package for euro symbol
kleing [Fri, 02 May 2003 16:39:38 +0200] rev 13947
removed package marvosym (breaks \Rightarrow)
reduced number of packages for "unusual symbols"
replaced \textzerooldstyle by \mathbf{0} etc to get normal sized numbers
kleing [Fri, 02 May 2003 15:19:36 +0200] rev 13946
more documentation for packages in root.tex
tuned IsaMakefile (make dependencies work)
paulson [Fri, 02 May 2003 10:25:42 +0200] rev 13945
moved Bij.thy from HOL/GroupTheory
paulson [Thu, 01 May 2003 11:54:18 +0200] rev 13944
new proofs about direct products, etc.
paulson [Thu, 01 May 2003 10:29:44 +0200] rev 13943
moving Bij.thy from GroupTheory to Algebra
berghofe [Thu, 01 May 2003 08:39:37 +0200] rev 13942
induct_impliesI is now unfolded.
ballarin [Wed, 30 Apr 2003 18:33:41 +0200] rev 13941
Unknown change.
ballarin [Wed, 30 Apr 2003 18:32:06 +0200] rev 13940
HOL-Algebra: New polynomial development added.
ballarin [Wed, 30 Apr 2003 18:31:38 +0200] rev 13939
HOL-Algebra: new dependencies.
ballarin [Wed, 30 Apr 2003 18:30:57 +0200] rev 13938
Simplifier: congruence rule update.
nipkow [Wed, 30 Apr 2003 17:53:47 +0200] rev 13937
added a thm
ballarin [Wed, 30 Apr 2003 10:01:35 +0200] rev 13936
Greatly extended CRing. Added Module.