Wed, 10 Mar 1999 10:42:11 +0100 |
paulson |
deleted obsolete comments
|
changeset |
files
|
Tue, 09 Mar 1999 12:20:22 +0100 |
wenzelm |
Present.theory_source;
|
changeset |
files
|
Tue, 09 Mar 1999 12:20:04 +0100 |
wenzelm |
begin/end_theory: presentation;
|
changeset |
files
|
Tue, 09 Mar 1999 12:19:25 +0100 |
wenzelm |
checkpoint -- basic functionality only;
|
changeset |
files
|
Tue, 09 Mar 1999 12:18:46 +0100 |
wenzelm |
added use_path;
|
changeset |
files
|
Tue, 09 Mar 1999 12:18:02 +0100 |
wenzelm |
IsarThy.begin/end_theory;
|
changeset |
files
|
Tue, 09 Mar 1999 12:17:40 +0100 |
wenzelm |
Present.theorem;
|
changeset |
files
|
Tue, 09 Mar 1999 12:13:58 +0100 |
wenzelm |
fixed add_path reset;
|
changeset |
files
|
Tue, 09 Mar 1999 12:13:11 +0100 |
wenzelm |
still fake, passes BrowserInfo;
|
changeset |
files
|
Tue, 09 Mar 1999 12:12:45 +0100 |
wenzelm |
HTML markup elements.
|
changeset |
files
|
Tue, 09 Mar 1999 12:12:02 +0100 |
wenzelm |
added html.ML, browser_info.ML;
|
changeset |
files
|
Tue, 09 Mar 1999 12:11:29 +0100 |
wenzelm |
token translation: real;
|
changeset |
files
|
Tue, 09 Mar 1999 12:11:00 +0100 |
wenzelm |
added strlen_real, setmp_margin;
|
changeset |
files
|
Tue, 09 Mar 1999 12:10:13 +0100 |
wenzelm |
tuned using nth_elem_string, exists_string;
|
changeset |
files
|
Tue, 09 Mar 1999 12:09:51 +0100 |
wenzelm |
added make, dir;
|
changeset |
files
|
Tue, 09 Mar 1999 12:09:22 +0100 |
wenzelm |
added mkdir;
|
changeset |
files
|
Tue, 09 Mar 1999 12:09:05 +0100 |
wenzelm |
added Buffer;
|
changeset |
files
|
Tue, 09 Mar 1999 12:08:50 +0100 |
wenzelm |
simple string buffers;
|
changeset |
files
|
Tue, 09 Mar 1999 12:08:08 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
Tue, 09 Mar 1999 12:07:52 +0100 |
wenzelm |
pretty_thm_no_quote;
|
changeset |
files
|
Tue, 09 Mar 1999 12:07:32 +0100 |
wenzelm |
HTML.setup;
|
changeset |
files
|
Tue, 09 Mar 1999 12:07:16 +0100 |
wenzelm |
added nth_elem_string, exists_string;
|
changeset |
files
|
Tue, 09 Mar 1999 12:06:09 +0100 |
wenzelm |
token translation: real;
|
changeset |
files
|
Tue, 09 Mar 1999 12:05:07 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 09 Mar 1999 11:09:01 +0100 |
paulson |
tidied
|
changeset |
files
|
Tue, 09 Mar 1999 11:01:39 +0100 |
paulson |
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
|
changeset |
files
|
Mon, 08 Mar 1999 13:49:53 +0100 |
nipkow |
Suc -> +1
|
changeset |
files
|
Mon, 08 Mar 1999 13:49:14 +0100 |
nipkow |
modified zip
|
changeset |
files
|
Fri, 05 Mar 1999 12:11:54 +0100 |
berghofe |
Fixed bug in add_datatype_axm:
|
changeset |
files
|
Thu, 04 Mar 1999 14:23:51 +0100 |
wenzelm |
fixed again;
|
changeset |
files
|
Wed, 03 Mar 1999 11:27:10 +0100 |
paulson |
expandshort
|
changeset |
files
|
Wed, 03 Mar 1999 11:26:36 +0100 |
paulson |
added UNITY/Extend
|
changeset |
files
|
Wed, 03 Mar 1999 11:15:18 +0100 |
paulson |
expandshort
|
changeset |
files
|
Wed, 03 Mar 1999 11:12:29 +0100 |
paulson |
tidied
|
changeset |
files
|
Wed, 03 Mar 1999 10:50:42 +0100 |
paulson |
UNITY fully working at last...
|
changeset |
files
|
Wed, 03 Mar 1999 10:36:24 +0100 |
paulson |
expandshort
|
changeset |
files
|
Wed, 03 Mar 1999 10:32:35 +0100 |
paulson |
new theory of extending the state space
|
changeset |
files
|
Mon, 01 Mar 1999 19:10:43 +0100 |
wenzelm |
fixed {ISABELLE};
|
changeset |
files
|
Mon, 01 Mar 1999 18:38:43 +0100 |
paulson |
removed the infernal States, eqStates, compatible, etc.
|
changeset |
files
|
Mon, 01 Mar 1999 18:37:52 +0100 |
paulson |
tidied
|
changeset |
files
|
Mon, 01 Mar 1999 18:37:23 +0100 |
paulson |
simpler proofs of congruence rules
|
changeset |
files
|
Mon, 01 Mar 1999 18:11:54 +0100 |
paulson |
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
|
changeset |
files
|
Mon, 01 Mar 1999 15:57:29 +0100 |
paulson |
simpler proofs of congruence rules
|
changeset |
files
|
Mon, 22 Feb 1999 10:21:59 +0100 |
paulson |
new image laws
|
changeset |
files
|
Mon, 22 Feb 1999 10:20:25 +0100 |
paulson |
added a commment on the "ext" rule
|
changeset |
files
|
Mon, 22 Feb 1999 10:19:32 +0100 |
paulson |
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
|
changeset |
files
|
Mon, 22 Feb 1999 10:16:59 +0100 |
paulson |
added rev_bexI
|
changeset |
files
|
Thu, 18 Feb 1999 12:15:55 +0100 |
wenzelm |
fixed order of multiple -m options;
|
changeset |
files
|
Thu, 18 Feb 1999 12:05:16 +0100 |
grobauer |
fixed geometry;
|
changeset |
files
|
Tue, 16 Feb 1999 10:54:55 +0100 |
paulson |
tidying in conjuntion with the TISSEC paper; replaced (unit option)
|
changeset |
files
|
Tue, 16 Feb 1999 10:50:35 +0100 |
paulson |
new theorem image_Union_eq
|
changeset |
files
|
Sat, 13 Feb 1999 22:08:54 +0100 |
wenzelm |
foldl_string;
|
changeset |
files
|
Fri, 12 Feb 1999 14:40:56 +0100 |
oheimb |
renamed space2 to spacespace
|
changeset |
files
|
Fri, 12 Feb 1999 13:56:21 +0100 |
wenzelm |
tuned pretty format lookup;
|
changeset |
files
|
Fri, 12 Feb 1999 13:55:54 +0100 |
wenzelm |
pretty_thm: quote terms (separately);
|
changeset |
files
|
Thu, 11 Feb 1999 21:25:21 +0100 |
wenzelm |
Symbol.output subject to print mode;
|
changeset |
files
|
Thu, 11 Feb 1999 21:19:56 +0100 |
wenzelm |
-m isabelle_font;
|
changeset |
files
|
Thu, 11 Feb 1999 21:18:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 11 Feb 1999 21:18:35 +0100 |
wenzelm |
Present.init;
|
changeset |
files
|
Thu, 11 Feb 1999 21:18:19 +0100 |
wenzelm |
init, finish;
|
changeset |
files
|
Thu, 11 Feb 1999 21:17:10 +0100 |
wenzelm |
proper handling of print_mode wrt. Pretty.sym;
|
changeset |
files
|
Thu, 11 Feb 1999 21:16:30 +0100 |
wenzelm |
added output_width;
|
changeset |
files
|
Thu, 11 Feb 1999 21:15:46 +0100 |
wenzelm |
sym: Symbol.output_width;
|
changeset |
files
|
Thu, 11 Feb 1999 21:15:27 +0100 |
wenzelm |
val appends: T list -> T;
|
changeset |
files
|
Thu, 11 Feb 1999 15:30:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 09 Feb 1999 10:47:21 +0100 |
paulson |
tidied; better error messages
|
changeset |
files
|
Tue, 09 Feb 1999 10:45:55 +0100 |
paulson |
new lemma surjD
|
changeset |
files
|
Mon, 08 Feb 1999 17:33:47 +0100 |
wenzelm |
Context.fetch, Context.setmp;
|
changeset |
files
|
Mon, 08 Feb 1999 17:33:24 +0100 |
wenzelm |
"files" keyword!
|
changeset |
files
|
Mon, 08 Feb 1999 17:33:03 +0100 |
wenzelm |
use: provide context;
|
changeset |
files
|
Mon, 08 Feb 1999 17:32:24 +0100 |
wenzelm |
tuned msgs;
|
changeset |
files
|
Mon, 08 Feb 1999 17:32:06 +0100 |
wenzelm |
tuned msg;
|
changeset |
files
|
Mon, 08 Feb 1999 17:31:50 +0100 |
wenzelm |
added fetch, fetch_theory;
|
changeset |
files
|
Mon, 08 Feb 1999 17:30:22 +0100 |
wenzelm |
~~;
|
changeset |
files
|
Mon, 08 Feb 1999 17:29:08 +0100 |
wenzelm |
path element specification '~~' refers to '$ISABELLE_HOME';
|
changeset |
files
|
Mon, 08 Feb 1999 15:55:35 +0100 |
wenzelm |
no deps on compile time sources;
|
changeset |
files
|
Mon, 08 Feb 1999 15:54:44 +0100 |
wenzelm |
isatool logo;
|
changeset |
files
|
Mon, 08 Feb 1999 15:53:56 +0100 |
wenzelm |
-i option;
|
changeset |
files
|
Mon, 08 Feb 1999 13:02:56 +0100 |
wenzelm |
updated (Stephan Merz);
|
changeset |
files
|
Mon, 08 Feb 1999 13:02:42 +0100 |
wenzelm |
updated TLA;
|
changeset |
files
|
Fri, 05 Feb 1999 21:26:20 +0100 |
wenzelm |
made MLWorks happy;
|
changeset |
files
|
Fri, 05 Feb 1999 21:14:17 +0100 |
wenzelm |
examples made separate dirs;
|
changeset |
files
|
Fri, 05 Feb 1999 21:12:45 +0100 |
wenzelm |
add_path;
|
changeset |
files
|
Fri, 05 Feb 1999 21:12:18 +0100 |
wenzelm |
Hyperreal made part of Real;
|
changeset |
files
|
Fri, 05 Feb 1999 21:11:41 +0100 |
wenzelm |
Session.use_dir: check parent;
|
changeset |
files
|
Fri, 05 Feb 1999 21:10:19 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
Fri, 05 Feb 1999 21:06:24 +0100 |
wenzelm |
more robust handling of theory context;
|
changeset |
files
|
Fri, 05 Feb 1999 21:04:58 +0100 |
wenzelm |
improved theory, context, update_context;
|
changeset |
files
|
Fri, 05 Feb 1999 21:04:31 +0100 |
wenzelm |
improved 'theory';
|
changeset |
files
|
Fri, 05 Feb 1999 21:03:33 +0100 |
wenzelm |
improved msg;
|
changeset |
files
|
Fri, 05 Feb 1999 21:03:06 +0100 |
wenzelm |
use_thy, update_thy: Context.save;
|
changeset |
files
|
Fri, 05 Feb 1999 21:02:17 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 05 Feb 1999 21:01:53 +0100 |
wenzelm |
time_use made pervasive;
|
changeset |
files
|
Fri, 05 Feb 1999 20:58:17 +0100 |
wenzelm |
use_dir: check parent, more robust exit;
|
changeset |
files
|
Fri, 05 Feb 1999 20:57:37 +0100 |
wenzelm |
more robust RC;
|
changeset |
files
|
Fri, 05 Feb 1999 20:57:18 +0100 |
wenzelm |
setmp: theory option;
|
changeset |
files
|
Fri, 05 Feb 1999 20:56:50 +0100 |
wenzelm |
Session.finish ();
|
changeset |
files
|
Fri, 05 Feb 1999 17:31:42 +0100 |
paulson |
tidied Schroeder-Bernstein proof
|
changeset |
files
|
Fri, 05 Feb 1999 17:31:04 +0100 |
paulson |
new surj rules
|
changeset |
files
|
Thu, 04 Feb 1999 18:31:57 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
Thu, 04 Feb 1999 18:18:19 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 04 Feb 1999 18:18:02 +0100 |
wenzelm |
include full paths in file info;
|
changeset |
files
|
Thu, 04 Feb 1999 18:17:20 +0100 |
wenzelm |
Symbol.use;
|
changeset |
files
|
Thu, 04 Feb 1999 18:17:01 +0100 |
wenzelm |
Symbol.use (eliminated Use.exit_use);
|
changeset |
files
|
Thu, 04 Feb 1999 18:16:22 +0100 |
wenzelm |
leave theory context after load_thy;
|
changeset |
files
|
Thu, 04 Feb 1999 18:15:53 +0100 |
wenzelm |
File.pwd, File.cd;
|
changeset |
files
|
Thu, 04 Feb 1999 18:15:20 +0100 |
wenzelm |
fixed file_info;
|
changeset |
files
|
Thu, 04 Feb 1999 18:15:01 +0100 |
wenzelm |
use, cd;
|
changeset |
files
|
Thu, 04 Feb 1999 18:14:40 +0100 |
wenzelm |
added 'use';
|
changeset |
files
|
Thu, 04 Feb 1999 18:14:27 +0100 |
wenzelm |
fail_safe close;
|
changeset |
files
|
Thu, 04 Feb 1999 18:13:10 +0100 |
wenzelm |
check_elem: allow ~, except for '~' and '~~';
|
changeset |
files
|
Thu, 04 Feb 1999 18:12:26 +0100 |
wenzelm |
removed use.ML;
|
changeset |
files
|
Thu, 04 Feb 1999 18:12:09 +0100 |
wenzelm |
removed General/use.ML;
|
changeset |
files
|
Wed, 03 Feb 1999 20:56:29 +0100 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
Wed, 03 Feb 1999 20:25:53 +0100 |
wenzelm |
check_thy: include ML stamp;
|
changeset |
files
|
Wed, 03 Feb 1999 20:25:01 +0100 |
wenzelm |
added join_info;
|
changeset |
files
|
Wed, 03 Feb 1999 17:36:55 +0100 |
wenzelm |
tidied load path handling;
|
changeset |
files
|
Wed, 03 Feb 1999 17:34:27 +0100 |
wenzelm |
add_path / reset_path;
|
changeset |
files
|
Wed, 03 Feb 1999 17:33:41 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 03 Feb 1999 17:33:20 +0100 |
wenzelm |
ThmDatabase.ml_store_thm;
|
changeset |
files
|