| Thu, 19 Oct 2000 21:22:44 +0200 |
wenzelm |
improved typedef;
|
changeset |
files
|
| Thu, 19 Oct 2000 21:22:05 +0200 |
wenzelm |
added theory for HOL type definitions;
|
changeset |
files
|
| Thu, 19 Oct 2000 21:21:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 19 Oct 2000 21:21:20 +0200 |
wenzelm |
added Tools/induct_attrib.ML;
|
changeset |
files
|
| Thu, 19 Oct 2000 21:20:53 +0200 |
wenzelm |
declare sym [elim?] in HOL.ML instead of Calculation.thy;
|
changeset |
files
|
| Thu, 19 Oct 2000 21:20:07 +0200 |
wenzelm |
tuned \isasymuniqex;
|
changeset |
files
|
| Thu, 19 Oct 2000 21:18:15 +0200 |
wenzelm |
split over two files: induct_attrib.ML, induct_method.ML;
|
changeset |
files
|
| Thu, 19 Oct 2000 02:19:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 19 Oct 2000 01:48:26 +0200 |
wenzelm |
use RecdefPackage.tcs_of;
|
changeset |
files
|
| Thu, 19 Oct 2000 01:47:50 +0200 |
wenzelm |
added tcs_of;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:58:07 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:44:52 +0200 |
wenzelm |
removed Library/Accessible_Part.ML;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:42:18 +0200 |
wenzelm |
use Multiset from HOL/Library;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:41:28 +0200 |
wenzelm |
use Accessible_Part from HOL/Library;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:40:58 +0200 |
wenzelm |
path_add "~~/src/HOL/Library";
|
changeset |
files
|
| Wed, 18 Oct 2000 23:40:38 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:40:17 +0200 |
wenzelm |
tuned declarations;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:39:49 +0200 |
wenzelm |
avoid "_" and "^" (more robust);
|
changeset |
files
|
| Wed, 18 Oct 2000 23:39:19 +0200 |
wenzelm |
removed Acc and Multiset (see HOL/Library);
|
changeset |
files
|
| Wed, 18 Oct 2000 23:38:41 +0200 |
wenzelm |
moved to HOL/Library;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:35:56 +0200 |
wenzelm |
MultisetOrder mmoved to HOL/Library;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:35:08 +0200 |
wenzelm |
moved to HOL/LIbrary;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:33:04 +0200 |
wenzelm |
added HOL/Library, rearranged several files;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:32:19 +0200 |
wenzelm |
moved to HOL/Library;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:31:16 +0200 |
wenzelm |
"The Supplemental Isabelle/HOL Library";
|
changeset |
files
|
| Wed, 18 Oct 2000 23:30:48 +0200 |
wenzelm |
added path_add;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:29:49 +0200 |
wenzelm |
A general ``while'' combinator (from main HOL);
|
changeset |
files
|
| Wed, 18 Oct 2000 23:29:13 +0200 |
wenzelm |
Quotient types;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:28:33 +0200 |
wenzelm |
Multisets (from HOL/Induct/Multiset and friends);
|
changeset |
files
|
| Wed, 18 Oct 2000 23:28:02 +0200 |
wenzelm |
The accessible part of a relation (from HOL/Induct/Acc);
|
changeset |
files
|
| Wed, 18 Oct 2000 23:27:16 +0200 |
wenzelm |
\isabellecontext: output_syms;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:26:42 +0200 |
wenzelm |
restart: do not reset theory loader path;
|
changeset |
files
|
| Wed, 18 Oct 2000 23:24:39 +0200 |
wenzelm |
* HOL/Library: a collection of generic theories to be used together
|
changeset |
files
|
| Wed, 18 Oct 2000 17:47:01 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 18 Oct 2000 17:19:24 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 18 Oct 2000 17:19:18 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 18 Oct 2000 12:30:59 +0200 |
paulson |
wellfounded -> well-founded
|
changeset |
files
|
| Tue, 17 Oct 2000 22:25:23 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 17 Oct 2000 22:25:03 +0200 |
wenzelm |
"Deriving rules";
|
changeset |
files
|
| Tue, 17 Oct 2000 22:22:56 +0200 |
wenzelm |
improved;
|
changeset |
files
|
| Tue, 17 Oct 2000 16:59:02 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 17 Oct 2000 13:28:57 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 17 Oct 2000 10:45:51 +0200 |
paulson |
renaming of contrapos rules
|
changeset |
files
|
| Tue, 17 Oct 2000 10:27:28 +0200 |
paulson |
tidied some awkward proofs
|
changeset |
files
|
| Tue, 17 Oct 2000 10:26:07 +0200 |
paulson |
tidying; removed unused rev_contra_subsetD
|
changeset |
files
|
| Tue, 17 Oct 2000 10:23:16 +0200 |
paulson |
restoration of "equalityI"; renaming of contrapos rules
|
changeset |
files
|
| Tue, 17 Oct 2000 10:21:12 +0200 |
paulson |
renaming of contrapos rules
|
changeset |
files
|
| Tue, 17 Oct 2000 10:20:43 +0200 |
paulson |
tidying and renaming of contrapos rules
|
changeset |
files
|
| Tue, 17 Oct 2000 08:41:42 +0200 |
oheimb |
cosmetics
|
changeset |
files
|
| Tue, 17 Oct 2000 08:00:46 +0200 |
nipkow |
added intermediate value thms
|
changeset |
files
|
| Tue, 17 Oct 2000 08:00:34 +0200 |
nipkow |
<= -> \<le>
|
changeset |
files
|
| Mon, 16 Oct 2000 20:33:15 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Mon, 16 Oct 2000 13:21:01 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 16 Oct 2000 10:59:35 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Sun, 15 Oct 2000 19:51:56 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 15 Oct 2000 19:51:19 +0200 |
wenzelm |
fixed \isasyminv;
|
changeset |
files
|
| Sun, 15 Oct 2000 19:50:59 +0200 |
wenzelm |
more elements;
|
changeset |
files
|
| Sun, 15 Oct 2000 19:50:35 +0200 |
wenzelm |
proper symbol markup with \isamath, \isatext;
|
changeset |
files
|
| Fri, 13 Oct 2000 18:32:08 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 13 Oct 2000 18:25:34 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 13 Oct 2000 18:02:08 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 13 Oct 2000 11:15:56 +0200 |
paulson |
renamed fp_Tarski to fp_unfold
|
changeset |
files
|
| Fri, 13 Oct 2000 10:49:05 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 13 Oct 2000 08:28:21 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 12 Oct 2000 18:44:35 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 12 Oct 2000 18:38:23 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 12 Oct 2000 18:09:06 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 12 Oct 2000 18:06:31 +0200 |
wenzelm |
induct -> lfp_induct;
|
changeset |
files
|
| Thu, 12 Oct 2000 17:54:22 +0200 |
wenzelm |
install default_handler for SIGINT initially as well;
|
changeset |
files
|
| Thu, 12 Oct 2000 17:52:44 +0200 |
wenzelm |
tuned syms;
|
changeset |
files
|
| Thu, 12 Oct 2000 17:48:47 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 12 Oct 2000 17:48:06 +0200 |
wenzelm |
accomodate Poly/ML 4.0;
|
changeset |
files
|
| Thu, 12 Oct 2000 17:47:32 +0200 |
wenzelm |
even smarter setup for several installations of Poly/ML 3.x and 4.0;
|
changeset |
files
|
| Thu, 12 Oct 2000 17:39:47 +0200 |
wenzelm |
tuned syms;
|
changeset |
files
|
| Thu, 12 Oct 2000 17:28:18 +0200 |
wenzelm |
removed nonsensical print statement;
|
changeset |
files
|
| Thu, 12 Oct 2000 13:01:19 +0200 |
nipkow |
induct -> lfp_induct
|
changeset |
files
|
| Thu, 12 Oct 2000 12:26:30 +0200 |
paulson |
tidied
|
changeset |
files
|
| Thu, 12 Oct 2000 12:19:15 +0200 |
paulson |
new theorem and SD-rule zmod_eq_0_iff
|
changeset |
files
|
| Thu, 12 Oct 2000 12:18:51 +0200 |
paulson |
delrules [r_into_rtrancl] required because the new I-rule made a step slow.
|
changeset |
files
|
| Thu, 12 Oct 2000 12:16:58 +0200 |
paulson |
tidied
|
changeset |
files
|
| Thu, 12 Oct 2000 12:16:22 +0200 |
paulson |
renamed ?Pa to ?Q in swap
|
changeset |
files
|
| Thu, 12 Oct 2000 12:15:59 +0200 |
paulson |
new I-rules r_into_rtrancl, r_into_trancl and a simpler proof
|
changeset |
files
|
| Thu, 12 Oct 2000 12:15:23 +0200 |
paulson |
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
|
changeset |
files
|
| Thu, 12 Oct 2000 11:47:17 +0200 |
wenzelm |
improved exhibit_interrupt;
|
changeset |
files
|
| Wed, 11 Oct 2000 19:06:36 +0200 |
wenzelm |
\isamath and \isatext: more abstract implementation of symbols;
|
changeset |
files
|
| Wed, 11 Oct 2000 13:39:52 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 11 Oct 2000 13:33:38 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 11 Oct 2000 13:20:27 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 11 Oct 2000 13:15:04 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 11 Oct 2000 12:52:56 +0200 |
wenzelm |
fixed \isastyleminor for "tt": \small;
|
changeset |
files
|
| Wed, 11 Oct 2000 10:44:42 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 11 Oct 2000 09:09:06 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 11 Oct 2000 00:03:22 +0200 |
wenzelm |
fixed 'clarify': CHANGED;
|
changeset |
files
|
| Tue, 10 Oct 2000 23:44:44 +0200 |
wenzelm |
fully enclose "\isadigit{...}";
|
changeset |
files
|
| Tue, 10 Oct 2000 23:43:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 10 Oct 2000 23:43:23 +0200 |
wenzelm |
AddXEs [someI_ex];
|
changeset |
files
|
| Tue, 10 Oct 2000 12:31:00 +0200 |
paulson |
added a section label
|
changeset |
files
|
| Mon, 09 Oct 2000 20:05:49 +0200 |
wenzelm |
fixed hrefs: index.html;
|
changeset |
files
|
| Mon, 09 Oct 2000 19:49:58 +0200 |
nipkow |
added rtranclIs
|
changeset |
files
|
| Mon, 09 Oct 2000 19:20:55 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 09 Oct 2000 17:40:47 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 09 Oct 2000 17:06:33 +0200 |
wenzelm |
tuned text;
|
changeset |
files
|
| Mon, 09 Oct 2000 14:10:55 +0200 |
nipkow |
ex_someI -> someI_ex
|
changeset |
files
|
| Mon, 09 Oct 2000 12:25:10 +0200 |
paulson |
simplified rtrancl_converse{I,D}
|
changeset |
files
|
| Mon, 09 Oct 2000 12:24:12 +0200 |
paulson |
got rid of a swap
|
changeset |
files
|
| Mon, 09 Oct 2000 12:23:45 +0200 |
paulson |
expandshort
|
changeset |
files
|
| Mon, 09 Oct 2000 10:18:21 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 09 Oct 2000 09:33:45 +0200 |
nipkow |
@ -> SOME
|
changeset |
files
|
| Sun, 08 Oct 2000 19:58:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Oct 2000 17:35:58 +0200 |
wenzelm |
final tuning;
Isabelle99-1
|
changeset |
files
|
| Fri, 06 Oct 2000 17:22:15 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Oct 2000 17:21:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Oct 2000 17:18:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Oct 2000 16:18:30 +0200 |
wenzelm |
* HOL/IMPP: extension of IMP with local variables and mutually
|
changeset |
files
|
| Fri, 06 Oct 2000 16:14:03 +0200 |
wenzelm |
updated, improved;
|
changeset |
files
|
| Fri, 06 Oct 2000 16:11:53 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Oct 2000 15:15:19 +0200 |
wenzelm |
draft for 99-1;
|
changeset |
files
|
| Fri, 06 Oct 2000 14:19:48 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Oct 2000 12:31:53 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 06 Oct 2000 01:21:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Oct 2000 01:04:56 +0200 |
wenzelm |
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
|
changeset |
files
|
| Thu, 05 Oct 2000 14:04:56 +0200 |
fleuriot |
Updated README file for HOL/Real
|
changeset |
files
|
| Wed, 04 Oct 2000 22:21:10 +0200 |
wenzelm |
new 'THEN' syntax;
|
changeset |
files
|
| Wed, 04 Oct 2000 21:06:01 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 04 Oct 2000 21:05:42 +0200 |
wenzelm |
added more stuff;
|
changeset |
files
|
| Wed, 04 Oct 2000 21:05:10 +0200 |
wenzelm |
improved @;
|
changeset |
files
|
| Wed, 04 Oct 2000 20:57:32 +0200 |
wenzelm |
'THEN', 'COMP': improved optional position arg;
|
changeset |
files
|
| Wed, 04 Oct 2000 20:55:57 +0200 |
wenzelm |
added "bracks";
|
changeset |
files
|
| Wed, 04 Oct 2000 17:35:45 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 03 Oct 2000 22:39:49 +0200 |
wenzelm |
Hoare logic in Isar;
|
changeset |
files
|
| Tue, 03 Oct 2000 22:37:16 +0200 |
wenzelm |
tuned deps;
|
changeset |
files
|
| Tue, 03 Oct 2000 22:36:22 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Oct 2000 22:35:44 +0200 |
wenzelm |
added Hoare;
|
changeset |
files
|
| Tue, 03 Oct 2000 22:35:19 +0200 |
wenzelm |
hide declaratations;
|
changeset |
files
|
| Tue, 03 Oct 2000 22:34:49 +0200 |
wenzelm |
added Isar_examples/Hoare.thy Isar_examples/HoareEx.thy;
|
changeset |
files
|
| Tue, 03 Oct 2000 18:57:11 +0200 |
wenzelm |
unsymbolized;
|
changeset |
files
|
| Tue, 03 Oct 2000 18:56:44 +0200 |
wenzelm |
tuned names;
|
changeset |
files
|
| Tue, 03 Oct 2000 18:55:23 +0200 |
wenzelm |
major cleanup -- improved typesetting;
|
changeset |
files
|
| Tue, 03 Oct 2000 18:45:36 +0200 |
wenzelm |
unsymbolize;
|
changeset |
files
|
| Tue, 03 Oct 2000 18:44:19 +0200 |
wenzelm |
eliminated \<oplus>;
|
changeset |
files
|
| Tue, 03 Oct 2000 18:40:25 +0200 |
wenzelm |
removed "symbols" syntax for constant "override";
|
changeset |
files
|
| Tue, 03 Oct 2000 18:39:31 +0200 |
wenzelm |
reorganized AxClasses;
|
changeset |
files
|
| Tue, 03 Oct 2000 18:34:20 +0200 |
wenzelm |
reorganized AxClasses;
|
changeset |
files
|
| Tue, 03 Oct 2000 18:30:56 +0200 |
wenzelm |
moved axclass tutorial examples to top dir;
|
changeset |
files
|
| Tue, 03 Oct 2000 11:26:54 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 03 Oct 2000 01:15:11 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 03 Oct 2000 01:14:52 +0200 |
wenzelm |
range declared as syntax;
|
changeset |
files
|
| Mon, 02 Oct 2000 15:13:32 +0200 |
wenzelm |
added == transitive rule (bad idea??);
|
changeset |
files
|
| Mon, 02 Oct 2000 15:12:34 +0200 |
wenzelm |
improved t.weak_case_cong text;
|
changeset |
files
|
| Mon, 02 Oct 2000 14:59:04 +0200 |
wenzelm |
delcongs weak_case_congs;
|
changeset |
files
|
| Mon, 02 Oct 2000 14:58:39 +0200 |
wenzelm |
renamed "None" to "NONE" (avoid clash with option type);
|
changeset |
files
|
| Mon, 02 Oct 2000 14:58:03 +0200 |
wenzelm |
qed "";
|
changeset |
files
|
| Mon, 02 Oct 2000 14:57:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 02 Oct 2000 14:44:05 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 02 Oct 2000 14:32:33 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 02 Oct 2000 14:25:10 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 02 Oct 2000 14:22:39 +0200 |
wenzelm |
export get_datatypes_sg;
|
changeset |
files
|
| Mon, 02 Oct 2000 14:21:12 +0200 |
wenzelm |
info: weak_case_cong;
|
changeset |
files
|
| Mon, 02 Oct 2000 12:35:48 +0200 |
nipkow |
separated expr and stmt
|
changeset |
files
|
| Sat, 30 Sep 2000 12:27:57 +0200 |
wenzelm |
isapar: \medskip;
|
changeset |
files
|
| Fri, 29 Sep 2000 18:02:24 +0200 |
berghofe |
Now some functions try to avoid name clashes when introducing new free
|
changeset |
files
|
| Fri, 29 Sep 2000 16:00:04 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 29 Sep 2000 11:51:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 28 Sep 2000 23:00:55 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 28 Sep 2000 23:00:11 +0200 |
wenzelm |
include log files;
|
changeset |
files
|
| Thu, 28 Sep 2000 19:10:19 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 28 Sep 2000 19:07:09 +0200 |
wenzelm |
some preliminary stuff on conversion;
|
changeset |
files
|
| Thu, 28 Sep 2000 19:06:46 +0200 |
wenzelm |
fixed ref;
|
changeset |
files
|
| Thu, 28 Sep 2000 14:49:15 +0200 |
wenzelm |
record proof tools: t.equality;
|
changeset |
files
|
| Thu, 28 Sep 2000 14:48:05 +0200 |
wenzelm |
isabelle -C;
|
changeset |
files
|
| Thu, 28 Sep 2000 14:47:42 +0200 |
wenzelm |
www.proofgeneral.org;
|
changeset |
files
|
| Thu, 28 Sep 2000 14:42:21 +0200 |
wenzelm |
fixed \<Union>, \<Inter> syntax;
|
changeset |
files
|
| Thu, 28 Sep 2000 14:41:48 +0200 |
wenzelm |
added COPYDB argument;
|
changeset |
files
|
| Thu, 28 Sep 2000 14:40:38 +0200 |
wenzelm |
option -C;
|
changeset |
files
|
| Thu, 28 Sep 2000 14:36:20 +0200 |
wenzelm |
Isabelle99-1 (October 2000);
|
changeset |
files
|
| Thu, 28 Sep 2000 14:36:02 +0200 |
wenzelm |
support copy option;
|
changeset |
files
|
| Thu, 28 Sep 2000 14:35:42 +0200 |
wenzelm |
./build -b -m Pure-copied Pure;
|
changeset |
files
|
| Thu, 28 Sep 2000 14:35:23 +0200 |
wenzelm |
only run quick_and_dirty version by default;
|
changeset |
files
|
| Thu, 28 Sep 2000 14:34:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 28 Sep 2000 13:12:23 +0200 |
paulson |
deleted card_0_empty_iff because it is the same as card_0_eq;
|
changeset |
files
|
| Wed, 27 Sep 2000 19:51:11 +0200 |
wenzelm |
THIS_IS_ISABELLE_BUILD;
|
changeset |
files
|
| Wed, 27 Sep 2000 19:39:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 27 Sep 2000 19:37:32 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Wed, 27 Sep 2000 19:36:31 +0200 |
wenzelm |
proper Hyperreal setup;
|
changeset |
files
|
| Wed, 27 Sep 2000 19:34:46 +0200 |
wenzelm |
more symbolic syntax (currently "input");
|
changeset |
files
|
| Wed, 27 Sep 2000 11:20:30 +0200 |
paulson |
exchanged the declaration of "seealso" and loading of "makeidx" because the
|
changeset |
files
|
| Tue, 26 Sep 2000 18:27:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 26 Sep 2000 18:24:01 +0200 |
wenzelm |
FAKE_BUILD="";
|
changeset |
files
|
| Tue, 26 Sep 2000 18:23:29 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 26 Sep 2000 18:15:21 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 26 Sep 2000 18:09:38 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 26 Sep 2000 17:34:33 +0200 |
wenzelm |
replaced by document (cannot maintain both);
|
changeset |
files
|
| Tue, 26 Sep 2000 17:07:28 +0200 |
wenzelm |
simplified;
|
changeset |
files
|
| Tue, 26 Sep 2000 17:06:16 +0200 |
wenzelm |
weblint;
|
changeset |
files
|
| Tue, 26 Sep 2000 17:05:20 +0200 |
wenzelm |
got rid of RPM;
|
changeset |
files
|
| Tue, 26 Sep 2000 17:05:01 +0200 |
wenzelm |
make Isabelle logic images for current platform;
|
changeset |
files
|
| Tue, 26 Sep 2000 17:04:17 +0200 |
wenzelm |
simplified;
|
changeset |
files
|
| Tue, 26 Sep 2000 17:03:52 +0200 |
wenzelm |
HOL/MicroJava;
|
changeset |
files
|
| Tue, 26 Sep 2000 17:02:51 +0200 |
wenzelm |
www.proofgeneral.org;
|
changeset |
files
|
| Tue, 26 Sep 2000 17:01:59 +0200 |
wenzelm |
updated url;
|
changeset |
files
|
| Tue, 26 Sep 2000 17:01:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 26 Sep 2000 16:42:24 +0200 |
paulson |
removed the obsolete (and badly named) inj_select
|
changeset |
files
|
| Mon, 25 Sep 2000 18:25:48 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 25 Sep 2000 16:51:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 25 Sep 2000 16:50:59 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 25 Sep 2000 16:34:29 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 25 Sep 2000 16:31:50 +0200 |
wenzelm |
tuned replacements;
|
changeset |
files
|
| Mon, 25 Sep 2000 12:11:45 +0200 |
wenzelm |
tuned auto paths;
|
changeset |
files
|
| Mon, 25 Sep 2000 12:08:49 +0200 |
kleing |
untabified for HTML
|
changeset |
files
|
| Mon, 25 Sep 2000 12:04:10 +0200 |
wenzelm |
include "Isabelle" link;
|
changeset |
files
|
| Sat, 23 Sep 2000 16:12:07 +0200 |
paulson |
tidied, removing obsolete "goal" commands
|
changeset |
files
|
| Sat, 23 Sep 2000 16:11:38 +0200 |
paulson |
new theorems and comment
|
changeset |
files
|
| Sat, 23 Sep 2000 16:08:23 +0200 |
paulson |
renaming the inverse image operator in HOL
|
changeset |
files
|
| Sat, 23 Sep 2000 16:02:01 +0200 |
paulson |
added compatibility relation: AllowedActs, Allowed, ok,
|
changeset |
files
|
| Fri, 22 Sep 2000 17:25:09 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Fri, 22 Sep 2000 17:24:36 +0200 |
wenzelm |
AddXIs [equal_intr_rule];
|
changeset |
files
|
| Fri, 22 Sep 2000 16:28:53 +0200 |
kleing |
added HTML syntax; added spaces in normal syntax for better documents
|
changeset |
files
|
| Fri, 22 Sep 2000 16:28:04 +0200 |
kleing |
added HTML syntax
|
changeset |
files
|
| Fri, 22 Sep 2000 13:16:24 +0200 |
kleing |
removed JVM/Store.ML, added theorem Digest in MicroJava
|
changeset |
files
|
| Fri, 22 Sep 2000 13:13:15 +0200 |
kleing |
lemma now in Store.thy
|
changeset |
files
|
| Fri, 22 Sep 2000 13:12:19 +0200 |
kleing |
converted to Isar, tuned
|
changeset |
files
|
| Thu, 21 Sep 2000 19:25:57 +0200 |
kleing |
tuned spacing for document generation
|
changeset |
files
|
| Thu, 21 Sep 2000 18:58:25 +0200 |
fleuriot |
*** empty log message ***
|
changeset |
files
|
| Thu, 21 Sep 2000 18:47:18 +0200 |
wenzelm |
renamed to Records.thy;
|
changeset |
files
|
| Thu, 21 Sep 2000 18:33:48 +0200 |
wenzelm |
improved \isachartilde for non-tt styles;
|
changeset |
files
|
| Thu, 21 Sep 2000 15:58:13 +0200 |
wenzelm |
renamed HOL/ex/Points to HOL/ex/Records;
|
changeset |
files
|
| Thu, 21 Sep 2000 14:55:46 +0200 |
kleing |
added height="100%" to stretch page to whole browser window
|
changeset |
files
|
| Thu, 21 Sep 2000 14:54:24 +0200 |
kleing |
added headline, "quick download", and mailing list archive
|
changeset |
files
|
| Thu, 21 Sep 2000 14:31:51 +0200 |
kleing |
added height="100%" to stretch page to whole browser window
|
changeset |
files
|
| Thu, 21 Sep 2000 12:26:37 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Thu, 21 Sep 2000 12:25:48 +0200 |
kleing |
Digest.thy as toplevel theory
|
changeset |
files
|
| Thu, 21 Sep 2000 12:25:07 +0200 |
kleing |
theorem digest of all MicroJava theorems, theories in alphabetical order
|
changeset |
files
|
| Thu, 21 Sep 2000 12:17:11 +0200 |
fleuriot |
New theories: construction of hypernaturals, nonstandard extensions,
|
changeset |
files
|
| Thu, 21 Sep 2000 12:13:36 +0200 |
kleing |
tuned, added lightweight BV to abstract, added Bali link
|
changeset |
files
|
| Thu, 21 Sep 2000 12:11:38 +0200 |
fleuriot |
Updated Files with new theorems
|
changeset |
files
|
| Thu, 21 Sep 2000 10:42:49 +0200 |
kleing |
unsymbolized
|
changeset |
files
|
| Wed, 20 Sep 2000 21:20:41 +0200 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Wed, 20 Sep 2000 21:20:26 +0200 |
wenzelm |
added "install" target;
|
changeset |
files
|
| Wed, 20 Sep 2000 21:20:01 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 20 Sep 2000 14:59:19 +0200 |
wenzelm |
tuned rpm command lines;
|
changeset |
files
|