Mon, 14 Feb 2000 20:49:08 +0100 |
wenzelm |
basic source deps;
|
changeset |
files
|
Mon, 14 Feb 2000 20:43:12 +0100 |
wenzelm |
easy_setup: fixed mksimps;
|
changeset |
files
|
Mon, 14 Feb 2000 20:42:02 +0100 |
wenzelm |
proof step: reset goal_facts;
|
changeset |
files
|
Mon, 14 Feb 2000 12:23:08 +0100 |
wenzelm |
mkdir -p $ISABELLE_BROWSER_INFO;
|
changeset |
files
|
Mon, 14 Feb 2000 11:23:57 +0100 |
wenzelm |
fixed prefer;
|
changeset |
files
|
Mon, 14 Feb 2000 11:23:44 +0100 |
wenzelm |
tuned msg;
|
changeset |
files
|
Sun, 13 Feb 2000 21:01:26 +0100 |
wenzelm |
added refine_end;
|
changeset |
files
|
Sun, 13 Feb 2000 21:00:02 +0100 |
wenzelm |
tuned attrib;
|
changeset |
files
|
Sun, 13 Feb 2000 20:58:13 +0100 |
wenzelm |
apply: observe facts;
|
changeset |
files
|
Sun, 13 Feb 2000 20:56:55 +0100 |
wenzelm |
prf_script commands made proper;
|
changeset |
files
|
Sun, 13 Feb 2000 20:54:12 +0100 |
wenzelm |
refine_end;
|
changeset |
files
|
Sun, 13 Feb 2000 20:52:58 +0100 |
wenzelm |
attrib: keyword_symid;
|
changeset |
files
|
Thu, 10 Feb 2000 20:54:40 +0100 |
wenzelm |
\isabellesimplestyle;
|
changeset |
files
|
Thu, 10 Feb 2000 20:54:18 +0100 |
wenzelm |
symid: include single symbolic char;
|
changeset |
files
|
Thu, 10 Feb 2000 20:52:59 +0100 |
wenzelm |
is_symbolic;
|
changeset |
files
|
Thu, 10 Feb 2000 13:36:23 +0100 |
wenzelm |
theorems [elim??] = sym;
|
changeset |
files
|
Thu, 10 Feb 2000 13:34:52 +0100 |
wenzelm |
added easy_setup;
|
changeset |
files
|
Thu, 10 Feb 2000 13:34:38 +0100 |
wenzelm |
add_judgment;
|
changeset |
files
|
Thu, 10 Feb 2000 11:08:42 +0100 |
paulson |
new thm and simprule inv_id
|
changeset |
files
|
Thu, 10 Feb 2000 11:03:54 +0100 |
paulson |
Cambridge-specific modifications
|
changeset |
files
|
Wed, 09 Feb 2000 14:35:23 +0100 |
wenzelm |
mirror dist page;
|
changeset |
files
|
Wed, 09 Feb 2000 14:12:14 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 09 Feb 2000 14:03:29 +0100 |
wenzelm |
mirror main page;
|
changeset |
files
|
Wed, 09 Feb 2000 13:43:35 +0100 |
kleing |
clearer "Obtaining" section
|
changeset |
files
|
Wed, 09 Feb 2000 12:30:25 +0100 |
wenzelm |
[df]rule methods;
|
changeset |
files
|
Wed, 09 Feb 2000 12:30:04 +0100 |
wenzelm |
document -c;
|
changeset |
files
|
Wed, 09 Feb 2000 12:29:03 +0100 |
wenzelm |
eliminated gif dir;
|
changeset |
files
|
Wed, 09 Feb 2000 12:28:44 +0100 |
wenzelm |
option -c;
|
changeset |
files
|
Wed, 09 Feb 2000 11:45:10 +0100 |
paulson |
updated the Client example
|
changeset |
files
|
Wed, 09 Feb 2000 11:43:53 +0100 |
paulson |
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
|
changeset |
files
|
Wed, 09 Feb 2000 11:42:26 +0100 |
paulson |
new thm order_less_imp_le
|
changeset |
files
|
Tue, 08 Feb 2000 22:28:30 +0100 |
wenzelm |
(then_)tac: assert_backward;
|
changeset |
files
|
Tue, 08 Feb 2000 20:17:41 +0100 |
wenzelm |
added -c option (beware!);
|
changeset |
files
|
Tue, 08 Feb 2000 20:14:58 +0100 |
wenzelm |
rename -p to -P;
|
changeset |
files
|
Tue, 08 Feb 2000 20:14:09 +0100 |
wenzelm |
added forget_proof;
|
changeset |
files
|
Tue, 08 Feb 2000 20:13:58 +0100 |
wenzelm |
added K.qed_global;
|
changeset |
files
|
Tue, 08 Feb 2000 20:12:36 +0100 |
wenzelm |
omit Primes;
|
changeset |
files
|
Mon, 07 Feb 2000 18:42:47 +0100 |
wenzelm |
(then_)apply: prove -> prove;
|
changeset |
files
|
Mon, 07 Feb 2000 18:40:40 +0100 |
wenzelm |
assert_no_chain;
|
changeset |
files
|
Mon, 07 Feb 2000 18:40:27 +0100 |
wenzelm |
refine_no_facts: recover goal_facts;
|
changeset |
files
|
Mon, 07 Feb 2000 18:39:53 +0100 |
wenzelm |
tuned prefer/defer;
|
changeset |
files
|
Mon, 07 Feb 2000 18:38:51 +0100 |
wenzelm |
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
|
changeset |
files
|
Mon, 07 Feb 2000 15:28:43 +0100 |
oheimb |
paper available
|
changeset |
files
|
Mon, 07 Feb 2000 15:14:02 +0100 |
paulson |
tidied some proofs
|
changeset |
files
|
Sat, 05 Feb 2000 17:31:53 +0100 |
kleing |
Branch: top elements of stack only need to be convertible (not equal)
|
changeset |
files
|
Sat, 05 Feb 2000 17:06:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 05 Feb 2000 16:59:50 +0100 |
wenzelm |
-I option;
|
changeset |
files
|
Sat, 05 Feb 2000 16:58:58 +0100 |
wenzelm |
-D PATH: dump generated document sources into PATH;
|
changeset |
files
|
Sat, 05 Feb 2000 16:57:02 +0100 |
wenzelm |
additional tex dump;
|
changeset |
files
|
Sat, 05 Feb 2000 16:54:27 +0100 |
wenzelm |
'.' == by this;
|
changeset |
files
|
Fri, 04 Feb 2000 21:53:36 +0100 |
wenzelm |
misc improvements;
|
changeset |
files
|
Fri, 04 Feb 2000 21:45:57 +0100 |
wenzelm |
added MicroJava/document;
|
changeset |
files
|
Fri, 04 Feb 2000 21:44:38 +0100 |
wenzelm |
added old_symbol_source;
|
changeset |
files
|
Fri, 04 Feb 2000 21:44:04 +0100 |
wenzelm |
Present.old_symbol_source;
|
changeset |
files
|
Fri, 04 Feb 2000 21:43:30 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 04 Feb 2000 21:37:23 +0100 |
wenzelm |
manually load session;
|
changeset |
files
|
Fri, 04 Feb 2000 21:36:13 +0100 |
wenzelm |
tuned syms;
|
changeset |
files
|
Fri, 04 Feb 2000 11:36:11 +0100 |
paulson |
new theorem gcd_add_mult
|
changeset |
files
|
Wed, 02 Feb 2000 20:19:25 +0100 |
wenzelm |
most_general_varify_tfrees all results;
|
changeset |
files
|
Wed, 02 Feb 2000 13:26:38 +0100 |
nipkow |
Rduced Class C <= Class D to C <= D.
|
changeset |
files
|