| Mon, 02 Feb 1998 12:56:24 +0100 |
paulson |
fixed WWW links
|
changeset |
files
|
| Mon, 02 Feb 1998 12:55:39 +0100 |
paulson |
Three new facts about Image
|
changeset |
files
|
| Mon, 02 Feb 1998 12:48:11 +0100 |
paulson |
Replaced \\1 by $1 as Perl itself asked me to...
|
changeset |
files
|
| Fri, 30 Jan 1998 12:31:59 +0100 |
paulson |
Fixed the description of recdef
|
changeset |
files
|
| Fri, 30 Jan 1998 11:34:06 +0100 |
wenzelm |
tuned msgs;
|
changeset |
files
|
| Fri, 30 Jan 1998 11:33:01 +0100 |
wenzelm |
improved tracing of rewrite rule application;
|
changeset |
files
|
| Fri, 30 Jan 1998 11:32:19 +0100 |
wenzelm |
removed dead messy code;
|
changeset |
files
|
| Fri, 30 Jan 1998 11:31:21 +0100 |
wenzelm |
added read_var;
|
changeset |
files
|
| Fri, 30 Jan 1998 11:01:49 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 23 Jan 1998 13:47:37 +0100 |
paulson |
Updated MOD reference
|
changeset |
files
|
| Wed, 21 Jan 1998 15:50:25 +0100 |
wenzelm |
added symbols syntax;
|
changeset |
files
|
| Tue, 20 Jan 1998 18:26:26 +0100 |
wenzelm |
reorganized into individual theories;
|
changeset |
files
|
| Mon, 19 Jan 1998 16:26:11 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 19 Jan 1998 16:25:36 +0100 |
wenzelm |
make images;
|
changeset |
files
|
| Thu, 15 Jan 1998 14:16:46 +0100 |
wenzelm |
tuned URL;
|
changeset |
files
|
| Thu, 15 Jan 1998 14:15:57 +0100 |
wenzelm |
polyml-3.1;
|
changeset |
files
|
| Thu, 15 Jan 1998 13:57:58 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Wed, 14 Jan 1998 16:38:04 +0100 |
mueller |
added thms wrt weakening and strengthening in Abstraction;
|
changeset |
files
|
| Wed, 14 Jan 1998 11:22:03 +0100 |
wenzelm |
New Jersey inactive;
Isabelle98
|
changeset |
files
|
| Wed, 14 Jan 1998 11:21:35 +0100 |
wenzelm |
HOL/record;
|
changeset |
files
|
| Wed, 14 Jan 1998 11:10:19 +0100 |
narasche |
error with instantiantion of sub-records removed
|
changeset |
files
|
| Wed, 14 Jan 1998 10:32:24 +0100 |
wenzelm |
added record.ML;
|
changeset |
files
|
| Wed, 14 Jan 1998 10:31:32 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 14 Jan 1998 10:30:44 +0100 |
wenzelm |
added unit and prod stuff;
|
changeset |
files
|
| Wed, 14 Jan 1998 10:30:01 +0100 |
wenzelm |
fixed Id;
|
changeset |
files
|
| Wed, 14 Jan 1998 10:28:21 +0100 |
wenzelm |
smlnj-110 factory default;
|
changeset |
files
|
| Wed, 14 Jan 1998 10:24:57 +0100 |
wenzelm |
added of_sort;
|
changeset |
files
|
| Tue, 13 Jan 1998 18:03:37 +0100 |
wenzelm |
added base_path;
|
changeset |
files
|
| Tue, 13 Jan 1998 14:31:09 +0100 |
mueller |
added simulations files to IOA;
|
changeset |
files
|
| Tue, 13 Jan 1998 14:26:21 +0100 |
mueller |
added forward simulation correectness;
|
changeset |
files
|
| Tue, 13 Jan 1998 10:40:38 +0100 |
narasche |
Simplification: sel make and update make
|
changeset |
files
|
| Mon, 12 Jan 1998 17:51:32 +0100 |
mueller |
added abstraction files;
|
changeset |
files
|
| Mon, 12 Jan 1998 17:51:05 +0100 |
mueller |
added further IOA liles;
|
changeset |
files
|
| Mon, 12 Jan 1998 17:49:12 +0100 |
wenzelm |
updated to Isabelle98;
|
changeset |
files
|
| Mon, 12 Jan 1998 17:48:55 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 12 Jan 1998 17:48:23 +0100 |
mueller |
added files containing temproal logic and abstraction;
|
changeset |
files
|
| Mon, 12 Jan 1998 17:26:34 +0100 |
wenzelm |
Delsimprocs nat_cancel;
|
changeset |
files
|
| Mon, 12 Jan 1998 17:26:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 12 Jan 1998 16:56:39 +0100 |
paulson |
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
|
changeset |
files
|
| Mon, 12 Jan 1998 15:47:43 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 12 Jan 1998 13:48:40 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 12 Jan 1998 13:32:47 +0100 |
wenzelm |
fixed author;
|
changeset |
files
|
| Sat, 10 Jan 1998 17:59:32 +0100 |
paulson |
Simplified proofs by omitting PA = {|XA, ...|} from RA2
|
changeset |
files
|
| Sat, 10 Jan 1998 17:58:42 +0100 |
paulson |
trivial tidy
|
changeset |
files
|
| Fri, 09 Jan 1998 20:28:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 09 Jan 1998 20:07:57 +0100 |
wenzelm |
automatic index.html patch;
|
changeset |
files
|
| Fri, 09 Jan 1998 14:28:20 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 09 Jan 1998 14:03:39 +0100 |
wenzelm |
tuned ISABELLE_TMP_PREFIX;
|
changeset |
files
|
| Fri, 09 Jan 1998 14:02:34 +0100 |
wenzelm |
thm_ord;
|
changeset |
files
|
| Fri, 09 Jan 1998 14:02:09 +0100 |
wenzelm |
eliminated make_ord;
|
changeset |
files
|
| Fri, 09 Jan 1998 14:01:48 +0100 |
wenzelm |
ISABELLE_TMP_PREFIX: $LOGNAME
|
changeset |
files
|
| Fri, 09 Jan 1998 13:49:20 +0100 |
wenzelm |
several minor updates;
|
changeset |
files
|
| Thu, 08 Jan 1998 19:04:33 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 08 Jan 1998 18:28:03 +0100 |
wenzelm |
index.html for Isabelle Distribution Area;
|
changeset |
files
|
| Thu, 08 Jan 1998 18:25:36 +0100 |
wenzelm |
updated to Isabelle98;
|
changeset |
files
|
| Thu, 08 Jan 1998 18:24:45 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 08 Jan 1998 18:19:48 +0100 |
wenzelm |
fixed thm_less;
|
changeset |
files
|
| Thu, 08 Jan 1998 18:10:34 +0100 |
paulson |
Expressed most Oops rules using Notes instead of Says, and other tidying
|
changeset |
files
|
| Thu, 08 Jan 1998 18:09:47 +0100 |
oheimb |
added split_paired_Ex to the implicit simpset
|
changeset |
files
|
| Thu, 08 Jan 1998 18:09:07 +0100 |
oheimb |
added select_equality to the implicit claset
|
changeset |
files
|
| Thu, 08 Jan 1998 18:08:43 +0100 |
oheimb |
added select_equality to the implicit claset
|
changeset |
files
|
| Thu, 08 Jan 1998 18:07:06 +0100 |
oheimb |
added newline at end of file
|
changeset |
files
|
| Thu, 08 Jan 1998 18:06:21 +0100 |
oheimb |
*** empty log message ***
|
changeset |
files
|
| Thu, 08 Jan 1998 18:03:36 +0100 |
oheimb |
streamlined specification of included theories
|
changeset |
files
|
| Thu, 08 Jan 1998 18:00:42 +0100 |
oheimb |
corrected Title
|
changeset |
files
|
| Thu, 08 Jan 1998 18:00:08 +0100 |
oheimb |
removed obsolete comment
|
changeset |
files
|
| Thu, 08 Jan 1998 17:56:32 +0100 |
oheimb |
added Univalent
|
changeset |
files
|
| Thu, 08 Jan 1998 17:47:22 +0100 |
oheimb |
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
|
changeset |
files
|
| Thu, 08 Jan 1998 17:44:50 +0100 |
oheimb |
added update_same, update_other, update_triv, and map_of_SomeD
|
changeset |
files
|
| Thu, 08 Jan 1998 17:42:26 +0100 |
oheimb |
replaced fn _ => by K
|
changeset |
files
|
| Thu, 08 Jan 1998 16:52:31 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Thu, 08 Jan 1998 11:24:46 +0100 |
paulson |
New rule: image_subset
|
changeset |
files
|
| Thu, 08 Jan 1998 11:23:18 +0100 |
paulson |
Restored the ciphertext in OR4 in order to make the spec closer to that in
|
changeset |
files
|
| Thu, 08 Jan 1998 11:21:45 +0100 |
paulson |
Tidied by adding more default simprules
|
changeset |
files
|
| Wed, 07 Jan 1998 13:55:54 +0100 |
wenzelm |
adapted to new split order;
|
changeset |
files
|
| Wed, 07 Jan 1998 13:55:29 +0100 |
wenzelm |
adapted to new sort function;
|
changeset |
files
|
| Wed, 07 Jan 1998 13:53:42 +0100 |
wenzelm |
improved targets;
|
changeset |
files
|
| Tue, 06 Jan 1998 12:32:43 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 05 Jan 1998 12:56:22 +0100 |
wenzelm |
added -u option (again);
|
changeset |
files
|
| Mon, 05 Jan 1998 10:47:10 +0100 |
paulson |
Now calls Blast_tac more often
|
changeset |
files
|
| Fri, 02 Jan 1998 18:47:31 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 02 Jan 1998 18:40:30 +0100 |
wenzelm |
feeder;
|
changeset |
files
|
| Fri, 02 Jan 1998 17:17:24 +0100 |
paulson |
Changed required by new blast_tac (the one that squashes flex-flex pairs)
|
changeset |
files
|
| Fri, 02 Jan 1998 17:16:39 +0100 |
paulson |
Blast_tac now squashes flex-flex pairs immediately
|
changeset |
files
|
| Fri, 02 Jan 1998 17:15:52 +0100 |
paulson |
New theorem image_subsetI
|
changeset |
files
|
| Fri, 02 Jan 1998 17:15:19 +0100 |
paulson |
Making proofs faster, especially using keysFor_parts_insert
|
changeset |
files
|
| Fri, 02 Jan 1998 13:24:53 +0100 |
wenzelm |
do require perl;
|
changeset |
files
|
| Fri, 02 Jan 1998 11:59:06 +0100 |
paulson |
Auto_tac now has type tactic, not unit->tactic
|
changeset |
files
|
| Fri, 02 Jan 1998 11:17:06 +0100 |
paulson |
Declared startTiming and endTiming
|
changeset |
files
|
| Wed, 31 Dec 1997 15:19:51 +0100 |
wenzelm |
use feeder to pipe into ML;
|
changeset |
files
|
| Wed, 31 Dec 1997 15:17:49 +0100 |
wenzelm |
removed -i option;
|
changeset |
files
|
| Tue, 30 Dec 1997 13:43:39 +0100 |
nipkow |
nth -> !
|
changeset |
files
|
| Tue, 30 Dec 1997 11:14:09 +0100 |
nipkow |
nth -> !
|
changeset |
files
|
| Mon, 29 Dec 1997 21:39:22 +0100 |
wenzelm |
feed isabelle session;
|
changeset |
files
|
| Mon, 29 Dec 1997 21:38:19 +0100 |
wenzelm |
commented out symboloutput.pl;
|
changeset |
files
|
| Mon, 29 Dec 1997 21:37:23 +0100 |
wenzelm |
added feeder.pl;
|
changeset |
files
|
| Mon, 29 Dec 1997 14:31:20 +0100 |
wenzelm |
pretty_name_space;
|
changeset |
files
|
| Mon, 29 Dec 1997 14:30:38 +0100 |
wenzelm |
removed declared;
|
changeset |
files
|
| Mon, 29 Dec 1997 14:29:34 +0100 |
wenzelm |
removed distinct_fst_string;
|
changeset |
files
|
| Sun, 28 Dec 1997 15:47:09 +0100 |
wenzelm |
improved error handling;
|
changeset |
files
|
| Sun, 28 Dec 1997 15:46:13 +0100 |
wenzelm |
fixed execute;
|
changeset |
files
|
| Sun, 28 Dec 1997 15:24:11 +0100 |
wenzelm |
made MLWorks happy;
|
changeset |
files
|
| Sun, 28 Dec 1997 15:11:54 +0100 |
wenzelm |
stderr to $LOG;
|
changeset |
files
|
| Sun, 28 Dec 1997 15:05:10 +0100 |
wenzelm |
Symtab.empty;
|
changeset |
files
|
| Sun, 28 Dec 1997 15:00:20 +0100 |
wenzelm |
improved internal representation;
|
changeset |
files
|
| Sun, 28 Dec 1997 14:58:56 +0100 |
wenzelm |
renamed Symtab.null to Symtab.empty;
|
changeset |
files
|
| Sun, 28 Dec 1997 14:58:06 +0100 |
wenzelm |
renamed Symtab.null to Symtab.empty;
|
changeset |
files
|
| Sun, 28 Dec 1997 14:56:44 +0100 |
wenzelm |
renamed Symtab.null to Symtab.empty;
|
changeset |
files
|
| Sun, 28 Dec 1997 14:56:09 +0100 |
wenzelm |
added >> : (theory -> theory) -> unit;
|
changeset |
files
|
| Sun, 28 Dec 1997 14:55:34 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 28 Dec 1997 14:55:20 +0100 |
wenzelm |
replaced symtab.ML by table.ML;
|
changeset |
files
|
| Sun, 28 Dec 1997 14:54:38 +0100 |
wenzelm |
renamed (is_)null to (is_)empty;
|
changeset |
files
|
| Sat, 27 Dec 1997 21:49:45 +0100 |
wenzelm |
Generic tables (lacking delete operation). Implemented as 2-3 trees.
|
changeset |
files
|
| Wed, 24 Dec 1997 12:38:40 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 24 Dec 1997 12:21:06 +0100 |
wenzelm |
export range_type;
|
changeset |
files
|
| Wed, 24 Dec 1997 12:20:54 +0100 |
wenzelm |
improved comment;
|
changeset |
files
|
| Wed, 24 Dec 1997 10:42:27 +0100 |
paulson |
More restrictive patterns to prevent changing comments
|
changeset |
files
|
| Wed, 24 Dec 1997 10:02:30 +0100 |
paulson |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
changeset |
files
|
| Tue, 23 Dec 1997 11:56:09 +0100 |
paulson |
Tidied using rev_iffD1
|
changeset |
files
|
| Tue, 23 Dec 1997 11:51:43 +0100 |
paulson |
Now Blast_tac works properly
|
changeset |
files
|
| Tue, 23 Dec 1997 11:50:36 +0100 |
paulson |
Tidied. Also better proof using new blast_tac
|
changeset |
files
|
| Tue, 23 Dec 1997 11:49:46 +0100 |
paulson |
Decremented subscript because of change to iffD1
|
changeset |
files
|
| Tue, 23 Dec 1997 11:47:13 +0100 |
paulson |
Tidied using rev_iffD1, etc
|
changeset |
files
|
| Tue, 23 Dec 1997 11:46:03 +0100 |
paulson |
Tidied using rev_iffD1
|
changeset |
files
|
| Tue, 23 Dec 1997 11:43:48 +0100 |
paulson |
Tidied using more default rules
|
changeset |
files
|
| Tue, 23 Dec 1997 11:41:12 +0100 |
paulson |
Overloading info for image
|
changeset |
files
|
| Tue, 23 Dec 1997 11:40:47 +0100 |
paulson |
tidied
|
changeset |
files
|
| Tue, 23 Dec 1997 11:40:18 +0100 |
paulson |
New rules rev_iffD{1,2}
|
changeset |
files
|
| Tue, 23 Dec 1997 11:39:03 +0100 |
paulson |
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
|
changeset |
files
|
| Tue, 23 Dec 1997 11:37:48 +0100 |
paulson |
New "obvious theorems"
|
changeset |
files
|
| Mon, 22 Dec 1997 12:22:06 +0100 |
paulson |
Added range-type for completeness
|
changeset |
files
|
| Mon, 22 Dec 1997 12:21:37 +0100 |
paulson |
New example
|
changeset |
files
|
| Mon, 22 Dec 1997 11:16:47 +0100 |
paulson |
New rules rev_iffD{1,2}
|
changeset |
files
|
| Fri, 19 Dec 1997 19:59:50 +0100 |
oheimb |
corrected removal to /tmp/tmp.c
|
changeset |
files
|
| Fri, 19 Dec 1997 19:57:28 +0100 |
oheimb |
added removal to /tmp/tmp.txt
|
changeset |
files
|
| Fri, 19 Dec 1997 13:31:08 +0100 |
narasche |
records without signature
|
changeset |
files
|
| Fri, 19 Dec 1997 13:30:21 +0100 |
narasche |
remove signatrue from records
|
changeset |
files
|
| Fri, 19 Dec 1997 12:16:32 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 19 Dec 1997 12:09:58 +0100 |
wenzelm |
new version;
|
changeset |
files
|
| Fri, 19 Dec 1997 12:09:08 +0100 |
wenzelm |
added record.ML;
|
changeset |
files
|
| Fri, 19 Dec 1997 12:00:24 +0100 |
narasche |
first version of records
|
changeset |
files
|
| Fri, 19 Dec 1997 10:33:59 +0100 |
wenzelm |
pasted old insertion sort (does not work with new sort function!)
|
changeset |
files
|
| Fri, 19 Dec 1997 10:33:24 +0100 |
wenzelm |
adapted to new sort function;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:31:13 +0100 |
wenzelm |
log file;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:30:27 +0100 |
wenzelm |
leading 0s;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:28:33 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:27:23 +0100 |
wenzelm |
adapted to new sort function;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:18:58 +0100 |
wenzelm |
log files;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:18:03 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:17:04 +0100 |
wenzelm |
added rev_order, make_ord;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:16:16 +0100 |
wenzelm |
term order;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:15:51 +0100 |
wenzelm |
term order stuff moved to term.ML;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:15:26 +0100 |
wenzelm |
log file;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:14:55 +0100 |
wenzelm |
'clean' target;
|
changeset |
files
|
| Fri, 19 Dec 1997 10:13:47 +0100 |
wenzelm |
adapted to new sort function;
|
changeset |
files
|
| Fri, 19 Dec 1997 09:58:42 +0100 |
wenzelm |
Term.termless;
|
changeset |
files
|
| Fri, 19 Dec 1997 09:58:03 +0100 |
wenzelm |
adapted to new sort function;
|
changeset |
files
|
| Fri, 19 Dec 1997 09:57:24 +0100 |
wenzelm |
removed maketest;
|
changeset |
files
|
| Thu, 18 Dec 1997 19:12:22 +0100 |
wenzelm |
showtime - print time.
|
changeset |
files
|
| Thu, 18 Dec 1997 12:50:58 +0100 |
oheimb |
added expand_split_asm
|
changeset |
files
|
| Thu, 18 Dec 1997 11:13:10 +0100 |
paulson |
UNIV_I no longer counts as safe
|
changeset |
files
|
| Wed, 17 Dec 1997 18:13:43 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 17 Dec 1997 17:59:18 +0100 |
wenzelm |
added mlworks;
|
changeset |
files
|
| Wed, 17 Dec 1997 17:51:39 +0100 |
wenzelm |
added MLWorks;
|
changeset |
files
|
| Wed, 17 Dec 1997 15:43:54 +0100 |
wenzelm |
misc improvements;
|
changeset |
files
|
| Wed, 17 Dec 1997 15:43:22 +0100 |
wenzelm |
tuned tmp file name;
|
changeset |
files
|
| Wed, 17 Dec 1997 14:57:26 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Wed, 17 Dec 1997 14:57:02 +0100 |
wenzelm |
added ML-Systems/mlworks.ML;
|
changeset |
files
|
| Tue, 16 Dec 1997 19:00:38 +0100 |
wenzelm |
MLWorks startup script (for 1.0r2 or later).
|
changeset |
files
|
| Tue, 16 Dec 1997 18:58:33 +0100 |
wenzelm |
renamed to mlworks.ML;
|
changeset |
files
|
| Tue, 16 Dec 1997 18:58:16 +0100 |
wenzelm |
Compatibility file for MLWorks version 1.0r2 or later.
|
changeset |
files
|
| Tue, 16 Dec 1997 17:58:03 +0100 |
wenzelm |
expandshort;
|
changeset |
files
|
| Tue, 16 Dec 1997 15:17:26 +0100 |
paulson |
Simplified proofs using rewrites for f``A where f is injective
|
changeset |
files
|
| Tue, 16 Dec 1997 15:15:38 +0100 |
paulson |
Simplified SpyKeys and ClientKeyExch as suggested by James Margetson
|
changeset |
files
|
| Tue, 16 Dec 1997 12:37:11 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Tue, 16 Dec 1997 12:24:31 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 16 Dec 1997 12:19:26 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Tue, 16 Dec 1997 12:17:48 +0100 |
wenzelm |
adapted from Larry's version;
|
changeset |
files
|
| Tue, 16 Dec 1997 12:17:22 +0100 |
wenzelm |
improved;
|
changeset |
files
|
| Mon, 15 Dec 1997 15:54:47 +0100 |
wenzelm |
improved COMMIT_RO;
|
changeset |
files
|
| Mon, 15 Dec 1997 15:32:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 15 Dec 1997 15:27:03 +0100 |
wenzelm |
polyml-3.1;
|
changeset |
files
|
| Mon, 15 Dec 1997 15:18:46 +0100 |
wenzelm |
make smlnj-110 default;
|
changeset |
files
|
| Mon, 15 Dec 1997 15:16:43 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 15 Dec 1997 14:40:13 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 15 Dec 1997 14:14:06 +0100 |
wenzelm |
No longer depend on theory context!
|
changeset |
files
|
| Sat, 13 Dec 1997 17:27:16 +0100 |
wenzelm |
version = "Isabelle98: Jan 1998";
|
changeset |
files
|
| Sat, 13 Dec 1997 17:22:41 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Sat, 13 Dec 1997 17:22:15 +0100 |
wenzelm |
smlnj-110;
|
changeset |
files
|
| Fri, 12 Dec 1997 22:43:10 +0100 |
wenzelm |
deleted smlnj-1.09.ML;
|
changeset |
files
|
| Fri, 12 Dec 1997 22:41:45 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 12 Dec 1997 22:41:15 +0100 |
wenzelm |
Compatibility file for Standard ML of New Jersey.
|
changeset |
files
|
| Fri, 12 Dec 1997 22:35:34 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 12 Dec 1997 18:10:59 +0100 |
wenzelm |
prepared for Isabelle98;
|
changeset |
files
|
| Fri, 12 Dec 1997 17:51:45 +0100 |
wenzelm |
added;
|
changeset |
files
|
| Fri, 12 Dec 1997 17:50:28 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 12 Dec 1997 17:23:01 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 12 Dec 1997 17:14:58 +0100 |
wenzelm |
tuned msg;
|
changeset |
files
|
| Fri, 12 Dec 1997 17:11:26 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 12 Dec 1997 17:11:05 +0100 |
wenzelm |
major update;
|
changeset |
files
|
| Fri, 12 Dec 1997 17:10:40 +0100 |
wenzelm |
SYNC;
|
changeset |
files
|
| Fri, 12 Dec 1997 10:46:09 +0100 |
paulson |
new blast_tac no longer works here
|
changeset |
files
|
| Fri, 12 Dec 1997 10:37:45 +0100 |
paulson |
More deterministic (?) contr_tac
|
changeset |
files
|
| Fri, 12 Dec 1997 10:34:21 +0100 |
paulson |
More deterministic and therefore faster (sometimes) proof reconstruction
|
changeset |
files
|
| Fri, 12 Dec 1997 10:32:45 +0100 |
paulson |
ugly patch for new Blast_tac
|
changeset |
files
|
| Fri, 12 Dec 1997 10:31:25 +0100 |
paulson |
Faster proof of mult_less_cancel2
|
changeset |
files
|
| Thu, 11 Dec 1997 13:15:06 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Dec 1997 10:30:33 +0100 |
paulson |
Tidied final proof
|
changeset |
files
|
| Thu, 11 Dec 1997 10:29:22 +0100 |
paulson |
Tidied proof of finite_subset_induct
|
changeset |
files
|
| Thu, 11 Dec 1997 10:28:04 +0100 |
paulson |
Got rid of mod2_neq_0
|
changeset |
files
|
| Mon, 08 Dec 1997 20:29:49 +0100 |
wenzelm |
\subsection{*Theory inclusion};
|
changeset |
files
|
| Mon, 08 Dec 1997 13:57:19 +0100 |
paulson |
Tidying to fix overfull lines, etc
|
changeset |
files
|
| Mon, 08 Dec 1997 13:56:49 +0100 |
paulson |
Comprehensive (??) list of bugs, fixed or not
|
changeset |
files
|
| Sun, 07 Dec 1997 16:09:55 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 07 Dec 1997 16:05:36 +0100 |
wenzelm |
added print_claset;
|
changeset |
files
|
| Sat, 06 Dec 1997 17:06:21 +0100 |
nipkow |
Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)).
|
changeset |
files
|
| Sat, 06 Dec 1997 17:05:41 +0100 |
nipkow |
Got rid of some preds and replaced some n~=0 by 0<n.
|
changeset |
files
|
| Sat, 06 Dec 1997 16:48:39 +0100 |
nipkow |
Cleaned up arithmetic mess.
|
changeset |
files
|
| Fri, 05 Dec 1997 18:46:18 +0100 |
wenzelm |
instantiate';
|
changeset |
files
|
| Fri, 05 Dec 1997 18:45:19 +0100 |
wenzelm |
changed typed_print_translation;
|
changeset |
files
|
| Fri, 05 Dec 1997 18:44:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 05 Dec 1997 17:31:01 +0100 |
wenzelm |
nat_cancel enabled by default;
|
changeset |
files
|
| Fri, 05 Dec 1997 17:20:25 +0100 |
wenzelm |
adapted proofs to cope with simprocs nat_cancel;
|
changeset |
files
|
| Fri, 05 Dec 1997 17:19:38 +0100 |
wenzelm |
improved arbitrary_def: we now really don't know nothing about it!
|
changeset |
files
|
| Fri, 05 Dec 1997 17:16:22 +0100 |
wenzelm |
use_thy no longer requires writable current directory;
|
changeset |
files
|
| Fri, 05 Dec 1997 17:14:36 +0100 |
wenzelm |
adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);
|
changeset |
files
|
| Fri, 05 Dec 1997 17:13:46 +0100 |
wenzelm |
simplification procedures nat_cancel enabled by default;
|
changeset |
files
|
| Fri, 05 Dec 1997 08:01:03 +0100 |
wenzelm |
tmp_name;
|
changeset |
files
|
| Thu, 04 Dec 1997 14:11:37 +0100 |
wenzelm |
added print_simpset;
|
changeset |
files
|
| Thu, 04 Dec 1997 13:50:43 +0100 |
wenzelm |
added is_base;
|
changeset |
files
|
| Thu, 04 Dec 1997 13:50:18 +0100 |
wenzelm |
added reset_context;
|
changeset |
files
|
| Thu, 04 Dec 1997 13:49:51 +0100 |
wenzelm |
added eq_set;
|
changeset |
files
|
| Thu, 04 Dec 1997 13:49:27 +0100 |
wenzelm |
moved global_names ref to Pure/ROOT.ML;
|
changeset |
files
|
| Thu, 04 Dec 1997 12:50:02 +0100 |
nipkow |
pred -> -1
|
changeset |
files
|
| Thu, 04 Dec 1997 12:44:37 +0100 |
nipkow |
pred n -> n-1
|
changeset |
files
|
| Thu, 04 Dec 1997 09:05:59 +0100 |
nipkow |
Simplified proofs.
|
changeset |
files
|
| Thu, 04 Dec 1997 09:05:39 +0100 |
nipkow |
Added thm mult_div_cancel
|
changeset |
files
|
| Wed, 03 Dec 1997 17:31:25 +0100 |
nipkow |
n ~= 0 should become 0 < n
|
changeset |
files
|
| Wed, 03 Dec 1997 17:25:43 +0100 |
nipkow |
Replaced n ~= 0 by 0 < n
|
changeset |
files
|
| Wed, 03 Dec 1997 12:55:04 +0100 |
wenzelm |
pass return code!!
|
changeset |
files
|
| Wed, 03 Dec 1997 11:42:45 +0100 |
paulson |
Fixed the treatment of substitution for equations, restricting occurrences of
|
changeset |
files
|
| Wed, 03 Dec 1997 11:00:24 +0100 |
paulson |
updated for latest Blast_tac, which treats equality differently
|
changeset |
files
|
| Wed, 03 Dec 1997 10:52:17 +0100 |
paulson |
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
|
changeset |
files
|
| Wed, 03 Dec 1997 10:50:02 +0100 |
paulson |
Tidying and some comments
|
changeset |
files
|
| Wed, 03 Dec 1997 10:49:33 +0100 |
paulson |
updated for latest Blast_tac, which treats equality differently
|
changeset |
files
|
| Wed, 03 Dec 1997 10:48:16 +0100 |
paulson |
Instantiated the one-point-rule quantifier simpprocs for FOL
|
changeset |
files
|
| Wed, 03 Dec 1997 10:47:13 +0100 |
paulson |
updated for latest Blast_tac, which fixes an equality bug
|
changeset |
files
|
| Wed, 03 Dec 1997 10:45:42 +0100 |
paulson |
Miniscoping now used except for one proof
|
changeset |
files
|
| Tue, 02 Dec 1997 12:42:59 +0100 |
wenzelm |
adapted to new term order;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:42:28 +0100 |
wenzelm |
tuned term order;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:41:29 +0100 |
wenzelm |
tuned trfuns types;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:41:02 +0100 |
wenzelm |
added prod_ord, dict_ord, list_ord;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:40:06 +0100 |
wenzelm |
File.tmp_name;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:39:03 +0100 |
wenzelm |
added tmp_name;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:38:39 +0100 |
wenzelm |
ISABELLE_TMP;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:38:08 +0100 |
wenzelm |
added context.ML;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:37:44 +0100 |
wenzelm |
Global contexts: session and theory.
|
changeset |
files
|
| Tue, 02 Dec 1997 12:37:22 +0100 |
wenzelm |
added Thy/context.ML;
|
changeset |
files
|
| Mon, 01 Dec 1997 18:27:43 +0100 |
wenzelm |
open;
|
changeset |
files
|
| Mon, 01 Dec 1997 18:27:06 +0100 |
wenzelm |
nat_cancel simprocs;
|
changeset |
files
|
| Mon, 01 Dec 1997 18:22:38 +0100 |
wenzelm |
ISABELLE_TMP_PREFIX;
|
changeset |
files
|
| Mon, 01 Dec 1997 18:22:02 +0100 |
wenzelm |
ISABELLE_TMP;
|
changeset |
files
|
| Mon, 01 Dec 1997 14:42:30 +0100 |
berghofe |
Added DiffCancelSums.
|
changeset |
files
|
| Mon, 01 Dec 1997 12:52:18 +0100 |
paulson |
New guarantee B_trusts_NS5, and tidying
|
changeset |
files
|
| Mon, 01 Dec 1997 12:50:04 +0100 |
paulson |
speed-up
|
changeset |
files
|
| Mon, 01 Dec 1997 08:59:40 +0100 |
narasche |
args for record data
|
changeset |
files
|
| Fri, 28 Nov 1997 16:17:30 +0100 |
nipkow |
Removed "open Mutil;"
|
changeset |
files
|
| Fri, 28 Nov 1997 11:00:42 +0100 |
paulson |
Added comments
|
changeset |
files
|
| Fri, 28 Nov 1997 10:59:14 +0100 |
paulson |
New timing functions startTiming and endTiming
|
changeset |
files
|
| Fri, 28 Nov 1997 10:54:13 +0100 |
paulson |
addsplits now in FOL, ZF too
|
changeset |
files
|
| Fri, 28 Nov 1997 10:52:32 +0100 |
paulson |
New example
|
changeset |
files
|
| Fri, 28 Nov 1997 10:52:04 +0100 |
paulson |
Printing of statistics including time for search & reconstruction
|
changeset |
files
|
| Fri, 28 Nov 1997 10:36:08 +0100 |
paulson |
New example
|
changeset |
files
|
| Fri, 28 Nov 1997 07:41:24 +0100 |
nipkow |
Removed dead code.
|
changeset |
files
|
| Fri, 28 Nov 1997 07:37:06 +0100 |
nipkow |
Moved the quantifier elimination simp procs into Provers.
|
changeset |
files
|
| Fri, 28 Nov 1997 07:35:47 +0100 |
nipkow |
Quantifier elimination procs.
|
changeset |
files
|
| Fri, 28 Nov 1997 07:35:10 +0100 |
nipkow |
Fixed the definition of `termord': is now antisymmetric.
|
changeset |
files
|
| Thu, 27 Nov 1997 19:39:02 +0100 |
wenzelm |
several minor updates;
|
changeset |
files
|
| Thu, 27 Nov 1997 19:37:36 +0100 |
wenzelm |
SYNC;
|
changeset |
files
|
| Thu, 27 Nov 1997 19:36:51 +0100 |
wenzelm |
removed read_cterms;
|
changeset |
files
|
| Thu, 27 Nov 1997 19:36:31 +0100 |
wenzelm |
fixed warning;
|
changeset |
files
|
| Thu, 27 Nov 1997 19:36:08 +0100 |
wenzelm |
removed same_thm;
|
changeset |
files
|
| Thu, 27 Nov 1997 14:05:25 +0100 |
paulson |
Tidying, mostly indentation
|
changeset |
files
|
| Thu, 27 Nov 1997 13:58:51 +0100 |
paulson |
Deleted some needless addSIs; got rid of a slow Blast_tac
|
changeset |
files
|
| Thu, 27 Nov 1997 13:38:06 +0100 |
wenzelm |
mk_norm_sum;
|
changeset |
files
|
| Wed, 26 Nov 1997 17:52:53 +0100 |
wenzelm |
separate lists of simprocs;
|
changeset |
files
|
| Wed, 26 Nov 1997 17:35:46 +0100 |
paulson |
Added rule impCE'
|
changeset |
files
|
| Wed, 26 Nov 1997 17:35:08 +0100 |
paulson |
Blast_tac can prove Pelletier\'s problem 46\!
|
changeset |
files
|
| Wed, 26 Nov 1997 17:32:52 +0100 |
paulson |
Tidying and using equalityCE instead of the slower equalityE
|
changeset |
files
|
| Wed, 26 Nov 1997 17:31:02 +0100 |
paulson |
The change from iffE to iffCE means fewer case splits in most cases. Very few
|
changeset |
files
|
| Wed, 26 Nov 1997 17:27:34 +0100 |
paulson |
Tidying
|
changeset |
files
|
| Wed, 26 Nov 1997 17:26:12 +0100 |
paulson |
Tidying and modification to cope with iffCE
|
changeset |
files
|
| Wed, 26 Nov 1997 17:23:18 +0100 |
paulson |
Added rule impCE'
|
changeset |
files
|
| Wed, 26 Nov 1997 17:16:48 +0100 |
paulson |
Changes to AddIs improve performance of Blast_tac
|
changeset |
files
|
| Wed, 26 Nov 1997 16:49:54 +0100 |
paulson |
Statistics
|
changeset |
files
|
| Wed, 26 Nov 1997 16:49:07 +0100 |
paulson |
updated comment
|
changeset |
files
|
| Wed, 26 Nov 1997 16:48:11 +0100 |
paulson |
Tidying and modification to cope with iffCE
|
changeset |
files
|
| Wed, 26 Nov 1997 16:45:54 +0100 |
wenzelm |
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
|
changeset |
files
|
| Wed, 26 Nov 1997 16:44:47 +0100 |
wenzelm |
added Arith provers;
|
changeset |
files
|
| Wed, 26 Nov 1997 16:44:25 +0100 |
wenzelm |
Setup various arithmetic proof procedures.
|
changeset |
files
|
| Wed, 26 Nov 1997 16:43:42 +0100 |
wenzelm |
added dest_nat;
|
changeset |
files
|
| Wed, 26 Nov 1997 16:42:56 +0100 |
wenzelm |
moved to Arith/;
|
changeset |
files
|
| Wed, 26 Nov 1997 16:42:37 +0100 |
wenzelm |
Cancel common constant factor from balanced exression.
|
changeset |
files
|
| Wed, 26 Nov 1997 16:42:19 +0100 |
wenzelm |
Cancel common summands of balanced expressions.
|
changeset |
files
|
| Wed, 26 Nov 1997 16:41:51 +0100 |
wenzelm |
removed conv_prover;
|
changeset |
files
|
| Wed, 26 Nov 1997 16:41:25 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 26 Nov 1997 16:38:04 +0100 |
wenzelm |
added crep_cterm;
|
changeset |
files
|
| Wed, 26 Nov 1997 16:37:43 +0100 |
wenzelm |
fixed type of thms_containing;
|
changeset |
files
|
| Wed, 26 Nov 1997 16:37:17 +0100 |
wenzelm |
added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a;
|
changeset |
files
|
| Wed, 26 Nov 1997 16:35:39 +0100 |
wenzelm |
cleaned signature;
|
changeset |
files
|
| Wed, 26 Nov 1997 16:34:13 +0100 |
wenzelm |
removed merge_opts;
|
changeset |
files
|
| Tue, 25 Nov 1997 17:56:49 +0100 |
mueller |
managed merge details;
|
changeset |
files
|
| Tue, 25 Nov 1997 16:34:20 +0100 |
mueller |
resolved merge conflict;
|
changeset |
files
|
| Mon, 24 Nov 1997 16:43:43 +0100 |
nipkow |
Added read_def_cterms for simultaneous reading/typing of terms under
|
changeset |
files
|
| Sat, 22 Nov 1997 13:27:02 +0100 |
wenzelm |
fixed warning;
|
changeset |
files
|
| Sat, 22 Nov 1997 13:26:43 +0100 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Sat, 22 Nov 1997 13:26:30 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 21 Nov 1997 15:47:39 +0100 |
wenzelm |
replaced by seq.ML;
|
changeset |
files
|
| Fri, 21 Nov 1997 15:41:27 +0100 |
wenzelm |
changed Pure/Sequence interface;
|
changeset |
files
|
| Fri, 21 Nov 1997 15:40:56 +0100 |
wenzelm |
SYNC;
|
changeset |
files
|
| Fri, 21 Nov 1997 15:37:02 +0100 |
wenzelm |
cd, use: path variables;
|
changeset |
files
|
| Fri, 21 Nov 1997 15:35:37 +0100 |
wenzelm |
comment;
|
changeset |
files
|
| Fri, 21 Nov 1997 15:34:15 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 21 Nov 1997 15:29:56 +0100 |
wenzelm |
changed Pure/Sequence interface -- isatool fixseq;
|
changeset |
files
|
| Fri, 21 Nov 1997 15:27:43 +0100 |
wenzelm |
changed Sequence interface (now Seq, in seq.ML);
|
changeset |
files
|
| Fri, 21 Nov 1997 15:26:22 +0100 |
wenzelm |
cd, use etc. now support path variables;
|
changeset |
files
|
| Fri, 21 Nov 1997 13:54:31 +0100 |
wenzelm |
fix references to obsolete Pure/Sequence structure;
|
changeset |
files
|
| Fri, 21 Nov 1997 12:15:27 +0100 |
paulson |
tidying
|
changeset |
files
|
| Fri, 21 Nov 1997 12:15:10 +0100 |
paulson |
analz_mono_contra_tac was wrong
|
changeset |
files
|
| Fri, 21 Nov 1997 12:14:47 +0100 |
paulson |
Deleted some useless comments
|
changeset |
files
|
| Fri, 21 Nov 1997 11:57:58 +0100 |
oheimb |
minor improvements of formulation and proofs
|
changeset |
files
|
| Fri, 21 Nov 1997 11:54:23 +0100 |
oheimb |
corrected INDUCT_FILES
|
changeset |
files
|
| Thu, 20 Nov 1997 16:24:05 +0100 |
wenzelm |
$ISABELLE_HOME/src;
|
changeset |
files
|
| Thu, 20 Nov 1997 15:48:32 +0100 |
wenzelm |
improved error msg;
|
changeset |
files
|
| Thu, 20 Nov 1997 15:38:51 +0100 |
wenzelm |
removed old note;
|
changeset |
files
|
| Thu, 20 Nov 1997 15:36:09 +0100 |
wenzelm |
adapted print methods;
|
changeset |
files
|
| Thu, 20 Nov 1997 15:30:37 +0100 |
wenzelm |
improved theorems print method: transfer_sg;
|
changeset |
files
|
| Thu, 20 Nov 1997 15:30:03 +0100 |
wenzelm |
init_data: improved print method;
|
changeset |
files
|
| Thu, 20 Nov 1997 15:28:48 +0100 |
wenzelm |
removed data.ML (made part of sign.ML);
|
changeset |
files
|
| Thu, 20 Nov 1997 15:07:19 +0100 |
wenzelm |
added type object = exn;
|
changeset |
files
|
| Thu, 20 Nov 1997 15:06:57 +0100 |
wenzelm |
added transfer_sg;
|
changeset |
files
|
| Thu, 20 Nov 1997 13:00:50 +0100 |
wenzelm |
fixed xstr token encoding;
|
changeset |
files
|
| Thu, 20 Nov 1997 12:59:20 +0100 |
wenzelm |
tuned infer_types interface;
|
changeset |
files
|
| Thu, 20 Nov 1997 12:51:55 +0100 |
wenzelm |
tuned infer_types interface;
|
changeset |
files
|
| Thu, 20 Nov 1997 12:51:31 +0100 |
wenzelm |
moved Sign.print_sg to display.ML;
|
changeset |
files
|
| Thu, 20 Nov 1997 12:50:57 +0100 |
wenzelm |
exported pretty_classrel, pretty_arity;
|
changeset |
files
|
| Thu, 20 Nov 1997 12:49:25 +0100 |
wenzelm |
added get_error: 'a error -> string option, get_ok: 'a error -> 'a option;
|
changeset |
files
|
| Thu, 20 Nov 1997 12:48:00 +0100 |
wenzelm |
added implode_xstr: string list -> string, explode_xstr: string -> string list;
|
changeset |
files
|
| Thu, 20 Nov 1997 11:55:39 +0100 |
paulson |
Now uses induct_tac
|
changeset |
files
|
| Thu, 20 Nov 1997 11:54:31 +0100 |
paulson |
Updated the NatSum example
|
changeset |
files
|
| Thu, 20 Nov 1997 11:53:51 +0100 |
paulson |
New, higher-level definition of \\out macro
|
changeset |
files
|
| Thu, 20 Nov 1997 11:03:53 +0100 |
paulson |
Speeded up the proof of succ_lt_induct_lemma
|
changeset |
files
|
| Thu, 20 Nov 1997 11:03:26 +0100 |
paulson |
Two new rewrites
|
changeset |
files
|
| Thu, 20 Nov 1997 10:55:27 +0100 |
paulson |
Got rid of some slow deepen_tac calls
|
changeset |
files
|
| Thu, 20 Nov 1997 10:54:04 +0100 |
paulson |
Renamed "overload" to "overloaded" for sml/nj compatibility
|
changeset |
files
|
| Thu, 20 Nov 1997 10:50:51 +0100 |
paulson |
No more makeatletter/other
|
changeset |
files
|
| Tue, 18 Nov 1997 16:37:25 +0100 |
paulson |
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
|
changeset |
files
|
| Tue, 18 Nov 1997 16:36:33 +0100 |
paulson |
The dtac was discarding information, though apparently no proofs were hurt
|
changeset |
files
|
| Tue, 18 Nov 1997 15:30:50 +0100 |
berghofe |
Fixed bug in inst_split.
|
changeset |
files
|
| Mon, 17 Nov 1997 15:40:25 +0100 |
wenzelm |
improved big_rec_name lookup;
|
changeset |
files
|
| Mon, 17 Nov 1997 10:50:03 +0100 |
paulson |
Updated comments. A bug causes MLWorks to use much
|
changeset |
files
|
| Mon, 17 Nov 1997 10:48:07 +0100 |
paulson |
Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
|
changeset |
files
|
| Mon, 17 Nov 1997 09:52:20 +0100 |
berghofe |
Tuned function mk_cntxt_splitthm.
|
changeset |
files
|
| Sun, 16 Nov 1997 16:18:31 +0100 |
nipkow |
Removed
|
changeset |
files
|
| Sat, 15 Nov 1997 18:41:06 +0100 |
nipkow |
Redesigned the decision procedures for (Abelian) groups and commutative rings.
|
changeset |
files
|
| Sat, 15 Nov 1997 13:10:52 +0100 |
nipkow |
Added
|
changeset |
files
|
| Fri, 14 Nov 1997 15:51:09 +0100 |
wenzelm |
merge_refs: check for different versions of theories;
|
changeset |
files
|
| Thu, 13 Nov 1997 17:55:27 +0100 |
wenzelm |
export read_raw_typ;
|
changeset |
files
|
| Thu, 13 Nov 1997 15:14:14 +0100 |
wenzelm |
fixed record parser;
|
changeset |
files
|
| Thu, 13 Nov 1997 12:43:17 +0100 |
wenzelm |
improved record syntax;
|
changeset |
files
|
| Thu, 13 Nov 1997 10:31:42 +0100 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Wed, 12 Nov 1997 18:58:50 +0100 |
oheimb |
added thin_refl to hyp_subst_tac
|
changeset |
files
|
| Wed, 12 Nov 1997 16:28:53 +0100 |
wenzelm |
refer to $ISABELLE_HOME/src;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:27:13 +0100 |
wenzelm |
structure BasisLibrary;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:26:05 +0100 |
wenzelm |
renamed to use.ML;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:25:45 +0100 |
wenzelm |
Redefine 'use' command in order to support path variable expansion,
|
changeset |
files
|
| Wed, 12 Nov 1997 16:25:35 +0100 |
wenzelm |
adapted to new Use, File structs;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:23:28 +0100 |
wenzelm |
added path variables;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:23:11 +0100 |
wenzelm |
File system operations.
|
changeset |
files
|
| Wed, 12 Nov 1997 16:22:59 +0100 |
wenzelm |
moved old file stuff from library.ML to Thy/browser_info.ML;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:22:47 +0100 |
wenzelm |
added file.ML, use.ML;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:22:10 +0100 |
wenzelm |
tuned warning msg;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:21:57 +0100 |
wenzelm |
major cleanup;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:21:26 +0100 |
wenzelm |
moved 'latex' from library.ML to goals.ML;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:21:15 +0100 |
wenzelm |
tuned prths;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:20:49 +0100 |
wenzelm |
structure BasisLibrary;
|
changeset |
files
|
| Wed, 12 Nov 1997 16:20:39 +0100 |
wenzelm |
added Thy/file.ML, Thy/use.ML;
|
changeset |
files
|
| Wed, 12 Nov 1997 12:38:12 +0100 |
oheimb |
renamed split_prem_tac to split_asm_tac
|
changeset |
files
|
| Wed, 12 Nov 1997 12:34:43 +0100 |
oheimb |
restored last version
|
changeset |
files
|
| Wed, 12 Nov 1997 12:30:15 +0100 |
oheimb |
simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm
|
changeset |
files
|
| Wed, 12 Nov 1997 12:24:55 +0100 |
oheimb |
renamed split_T_case_prem to split_T_case_asm
|
changeset |
files
|
| Wed, 12 Nov 1997 12:23:37 +0100 |
oheimb |
renamed split_prem_tac to split_asm_tac
|
changeset |
files
|
| Wed, 12 Nov 1997 12:22:56 +0100 |
oheimb |
renamed split_prem_tac to split_asm_tac
|
changeset |
files
|
| Tue, 11 Nov 1997 16:04:14 +0100 |
paulson |
Fixed indentation
|
changeset |
files
|
| Tue, 11 Nov 1997 15:45:56 +0100 |
paulson |
Rationalized the theorem if_image_distrib.
|
changeset |
files
|
| Tue, 11 Nov 1997 12:30:51 +0100 |
paulson |
Fixed indentation
|
changeset |
files
|
| Tue, 11 Nov 1997 11:16:18 +0100 |
paulson |
Fixed spelling error
|
changeset |
files
|
| Tue, 11 Nov 1997 11:15:51 +0100 |
paulson |
Made some proofs more robust
|
changeset |
files
|
| Tue, 11 Nov 1997 11:12:37 +0100 |
paulson |
Now applies "map negOfGoal" to lits when expanding haz rules.
|
changeset |
files
|
| Mon, 10 Nov 1997 15:25:12 +0100 |
wenzelm |
ASCII-fied;
|
changeset |
files
|
| Mon, 10 Nov 1997 15:06:58 +0100 |
oheimb |
polished definition of find_index_eq
|
changeset |
files
|
| Mon, 10 Nov 1997 15:05:41 +0100 |
wenzelm |
check files for non-ASCII characters;
|
changeset |
files
|
| Mon, 10 Nov 1997 14:57:31 +0100 |
oheimb |
replaced 8bit characters
|
changeset |
files
|
| Mon, 10 Nov 1997 14:30:35 +0100 |
wenzelm |
fixed LAM<...> syntax;
|
changeset |
files
|
| Mon, 10 Nov 1997 11:47:32 +0100 |
wenzelm |
fixed spelling;
|
changeset |
files
|
| Fri, 07 Nov 1997 18:05:25 +0100 |
oheimb |
added split_prem_tac
|
changeset |
files
|
| Fri, 07 Nov 1997 18:02:15 +0100 |
oheimb |
changed libraray function find to find_index_eq, currying it
|
changeset |
files
|
| Fri, 07 Nov 1997 17:51:26 +0100 |
oheimb |
added contrapos
|
changeset |
files
|
| Fri, 07 Nov 1997 17:51:10 +0100 |
oheimb |
added contrapos2
|
changeset |
files
|
| Fri, 07 Nov 1997 15:24:58 +0100 |
oheimb |
added exists_Const
|
changeset |
files
|
| Fri, 07 Nov 1997 08:25:02 +0100 |
nipkow |
Each datatype t now proves a theorem split_t_case_prem
|
changeset |
files
|
| Thu, 06 Nov 1997 16:44:35 +0100 |
wenzelm |
Perl no longer optional;
|
changeset |
files
|
| Thu, 06 Nov 1997 16:41:08 +0100 |
wenzelm |
deriv: eliminated references to theory;
|
changeset |
files
|
| Thu, 06 Nov 1997 16:40:45 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 06 Nov 1997 12:27:12 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 06 Nov 1997 10:29:37 +0100 |
paulson |
hyp_subst_tac checks if the equality has type variables and uses a suitable
|
changeset |
files
|
| Thu, 06 Nov 1997 10:28:20 +0100 |
paulson |
subgoal_tac displays a warning if the new subgoal has type variables
|
changeset |
files
|
| Wed, 05 Nov 1997 19:40:50 +0100 |
wenzelm |
mkdir -p bin;
|
changeset |
files
|
| Wed, 05 Nov 1997 19:39:34 +0100 |
wenzelm |
Tools/8bit: ./mk;
|
changeset |
files
|
| Wed, 05 Nov 1997 18:31:14 +0100 |
oheimb |
*** empty log message ***
|
changeset |
files
|
| Wed, 05 Nov 1997 16:37:22 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 05 Nov 1997 15:49:38 +0100 |
oheimb |
abandoned generation of tmp files
|
changeset |
files
|
| Wed, 05 Nov 1997 15:48:24 +0100 |
oheimb |
various improvements
|
changeset |
files
|
| Wed, 05 Nov 1997 15:47:27 +0100 |
oheimb |
reflecting changes of isa2latex
|
changeset |
files
|
| Wed, 05 Nov 1997 15:45:51 +0100 |
oheimb |
several minor improvements
|
changeset |
files
|
| Wed, 05 Nov 1997 15:42:30 +0100 |
oheimb |
added ax2isa
|
changeset |
files
|
| Wed, 05 Nov 1997 15:42:07 +0100 |
oheimb |
added ax2isa
|
changeset |
files
|
| Wed, 05 Nov 1997 15:38:40 +0100 |
oheimb |
added isabelle14 and isabelle24
|
changeset |
files
|
| Wed, 05 Nov 1997 15:36:54 +0100 |
oheimb |
removed gererated files
|
changeset |
files
|
| Wed, 05 Nov 1997 15:36:40 +0100 |
oheimb |
added entry for manual
|
changeset |
files
|
| Wed, 05 Nov 1997 15:36:01 +0100 |
oheimb |
*** empty log message ***
|
changeset |
files
|
| Wed, 05 Nov 1997 14:00:49 +0100 |
paulson |
Now introduces Safe_tac
|
changeset |
files
|
| Wed, 05 Nov 1997 13:50:59 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
changeset |
files
|
| Wed, 05 Nov 1997 13:50:16 +0100 |
paulson |
Adapted to removal of UN1_I, etc
|
changeset |
files
|
| Wed, 05 Nov 1997 13:45:01 +0100 |
paulson |
Adapted to removal of UN1_I, etc
|
changeset |
files
|
| Wed, 05 Nov 1997 13:32:07 +0100 |
paulson |
UNIV now a constant; UNION1, INTER1 now translations and no longer have
|
changeset |
files
|
| Wed, 05 Nov 1997 13:29:47 +0100 |
paulson |
Expandshort; new theorem le_square
|
changeset |
files
|
| Wed, 05 Nov 1997 13:27:58 +0100 |
paulson |
generalized UNION1 to UNION
|
changeset |
files
|
| Wed, 05 Nov 1997 13:27:29 +0100 |
paulson |
Tidied Key_supply3
|
changeset |
files
|
| Wed, 05 Nov 1997 13:26:19 +0100 |
paulson |
fixed comment
|
changeset |
files
|
| Wed, 05 Nov 1997 13:25:34 +0100 |
paulson |
UNIV & UNION1
|
changeset |
files
|
| Wed, 05 Nov 1997 13:23:46 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
changeset |
files
|
| Wed, 05 Nov 1997 13:14:15 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
changeset |
files
|
| Wed, 05 Nov 1997 11:49:34 +0100 |
wenzelm |
adapted typed_print_translation;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:49:07 +0100 |
wenzelm |
tuned record_info;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:45:51 +0100 |
wenzelm |
fixed exception OPTION;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:43:37 +0100 |
wenzelm |
adapted pure_trfunsT;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:42:19 +0100 |
wenzelm |
print translation: added show_sorts argument;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:41:46 +0100 |
wenzelm |
adapted syn_ext_trfunsT;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:41:18 +0100 |
wenzelm |
adapted extend_trfunsT;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:40:51 +0100 |
wenzelm |
fixed exception OPTION;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:40:23 +0100 |
wenzelm |
added TYPE syntax;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:35:07 +0100 |
wenzelm |
fixed exception OPTION;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:34:44 +0100 |
wenzelm |
adapted add_trfunsT;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:33:45 +0100 |
wenzelm |
adapted add_trfunsT;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:33:05 +0100 |
wenzelm |
fixed exception OPTION;
|
changeset |
files
|
| Wed, 05 Nov 1997 11:19:15 +0100 |
wenzelm |
base root = "";
|
changeset |
files
|
| Wed, 05 Nov 1997 09:08:35 +0100 |
nipkow |
Added an alternativ version of AutoChopper and a theory for the conversion of
|
changeset |
files
|
| Tue, 04 Nov 1997 20:52:20 +0100 |
oheimb |
removed redundant ball_image
|
changeset |
files
|
| Tue, 04 Nov 1997 20:50:35 +0100 |
oheimb |
removed redundant ball_empty and bex_empty (see equalities.ML)
|
changeset |
files
|
| Tue, 04 Nov 1997 20:49:45 +0100 |
oheimb |
added several theorems
|
changeset |
files
|
| Tue, 04 Nov 1997 20:48:38 +0100 |
oheimb |
added the, option_map, and case analysis theorems
|
changeset |
files
|
| Tue, 04 Nov 1997 20:47:38 +0100 |
oheimb |
added zip and nodup
|
changeset |
files
|
| Tue, 04 Nov 1997 20:46:56 +0100 |
oheimb |
added theorems for Eps
|
changeset |
files
|
| Tue, 04 Nov 1997 17:16:26 +0100 |
wenzelm |
tuned usage;
|
changeset |
files
|
| Tue, 04 Nov 1997 17:12:13 +0100 |
wenzelm |
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
|
changeset |
files
|
| Tue, 04 Nov 1997 16:57:52 +0100 |
wenzelm |
tuned to make non-Poly/MLs happy;
|
changeset |
files
|
| Tue, 04 Nov 1997 16:49:35 +0100 |
wenzelm |
tuned 'records' stuff;
|
changeset |
files
|
| Tue, 04 Nov 1997 16:46:02 +0100 |
wenzelm |
added pretty_ctyp;
|
changeset |
files
|
| Tue, 04 Nov 1997 16:21:52 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 04 Nov 1997 16:17:04 +0100 |
wenzelm |
type object = exn (enhance readability);
|
changeset |
files
|
| Tue, 04 Nov 1997 15:16:23 +0100 |
oheimb |
*** empty log message ***
|
changeset |
files
|
| Tue, 04 Nov 1997 14:40:29 +0100 |
oheimb |
* removed "axioms" and "generated by" section
|
changeset |
files
|
| Tue, 04 Nov 1997 14:37:51 +0100 |
oheimb |
simplified (and corrected) syntax definition of fapp
|
changeset |
files
|
| Tue, 04 Nov 1997 14:09:37 +0100 |
narasche |
data kinds 'datatypes', data kinds 'records' added
|
changeset |
files
|
| Tue, 04 Nov 1997 13:35:13 +0100 |
wenzelm |
removed old datatype_info;
|
changeset |
files
|
| Tue, 04 Nov 1997 13:31:14 +0100 |
wenzelm |
added Thy/path.ML;
|
changeset |
files
|
| Tue, 04 Nov 1997 12:59:01 +0100 |
nipkow |
Logic.loops -> Logic.rewrite_rule_ok
|
changeset |
files
|
| Tue, 04 Nov 1997 12:58:10 +0100 |
nipkow |
logic: loops -> rewrite_rule_ok
|
changeset |
files
|
| Tue, 04 Nov 1997 12:46:50 +0100 |
wenzelm |
added path.ML;
|
changeset |
files
|