wenzelm [Sun, 27 Feb 2000 15:25:31 +0100] rev 8304
even better induct setup;
wenzelm [Sun, 27 Feb 2000 15:23:28 +0100] rev 8303
early setup of induct_method;
wenzelm [Sun, 27 Feb 2000 15:22:14 +0100] rev 8302
added dest_conj;
wenzelm [Sun, 27 Feb 2000 15:21:13 +0100] rev 8301
theorems [trans] = rev_mp mp;
wenzelm [Sun, 27 Feb 2000 15:15:52 +0100] rev 8300
use NetRules;
wenzelm [Sun, 27 Feb 2000 15:13:44 +0100] rev 8299
added major_prem_of;
wenzelm [Sun, 27 Feb 2000 15:07:53 +0100] rev 8298
added Isar/net_rules.ML;
wenzelm [Thu, 24 Feb 2000 21:33:32 +0100] rev 8297
simplified induct method;
wenzelm [Thu, 24 Feb 2000 16:04:25 +0100] rev 8296
tuned;
wenzelm [Thu, 24 Feb 2000 16:01:34 +0100] rev 8295
induct method: implicit rule;
wenzelm [Thu, 24 Feb 2000 16:00:28 +0100] rev 8294
rN = "record";
wenzelm [Thu, 24 Feb 2000 16:00:09 +0100] rev 8293
all_cases / all_inducts;
wenzelm [Thu, 24 Feb 2000 15:59:44 +0100] rev 8292
workaround res_inst_tac/lift_inst_rule bug by explicit type contraint;
wenzelm [Thu, 24 Feb 2000 15:58:10 +0100] rev 8291
capply, cabs: Sign.nodup_vars;
wenzelm [Thu, 24 Feb 2000 15:57:36 +0100] rev 8290
nodup_vars: fixed omission of 2 minor cases; account for Frees as well;
wenzelm [Thu, 24 Feb 2000 15:34:49 +0100] rev 8289
tuned generated TeX code;
nipkow [Thu, 24 Feb 2000 08:56:36 +0100] rev 8288
renamed a lemma
nipkow [Thu, 24 Feb 2000 08:55:37 +0100] rev 8287
Added and renamed a lemma.
paulson [Wed, 23 Feb 2000 10:45:08 +0100] rev 8286
not working yet. partial conversion to use "rename" instead of "extend"
paulson [Wed, 23 Feb 2000 10:43:02 +0100] rev 8285
new theorems inj_iff, surj_iff
paulson [Wed, 23 Feb 2000 10:41:37 +0100] rev 8284
new reference korf85
wenzelm [Tue, 22 Feb 2000 21:53:17 +0100] rev 8283
* Pure now provides its own version of intro/elim/dest attributes;
useful for building new logics, but beware of confusion with the
Provers/classical ones!
* HOL: removed "case_split" thm binding, should use "cases" proof
method anyway;
* tuned syntax of "induct" method;
* new "cases" method for propositions, inductive sets and types;
* HOL/records: admit "r" as field name;
wenzelm [Tue, 22 Feb 2000 21:51:25 +0100] rev 8282
tuned syntax wrapper;
wenzelm [Tue, 22 Feb 2000 21:50:02 +0100] rev 8281
tuned "induct" syntax;
wenzelm [Tue, 22 Feb 2000 21:49:34 +0100] rev 8280
"cases" method;
wenzelm [Tue, 22 Feb 2000 21:48:50 +0100] rev 8279
added cases_tac;
wenzelm [Tue, 22 Feb 2000 21:48:24 +0100] rev 8278
induct: tuned syntax;
added cases method;
wenzelm [Tue, 22 Feb 2000 21:45:20 +0100] rev 8277
added cases_of, cases;
wenzelm [Tue, 22 Feb 2000 21:39:38 +0100] rev 8276
removed case_split thm binding;
wenzelm [Tue, 22 Feb 2000 21:39:01 +0100] rev 8275
added boolN;
wenzelm [Tue, 22 Feb 2000 20:16:07 +0100] rev 8274
proper variant names (admit field "r");
paulson [Tue, 22 Feb 2000 10:51:13 +0100] rev 8273
three easy new examples
wenzelm [Mon, 21 Feb 2000 14:10:21 +0100] rev 8272
tuned footnote;
wenzelm [Mon, 21 Feb 2000 14:09:40 +0100] rev 8271
HOL/record: fixed select-update simplification procedure to handle
extended records as well;
wenzelm [Mon, 21 Feb 2000 14:09:18 +0100] rev 8270
var: skolem;
wenzelm [Mon, 21 Feb 2000 14:08:15 +0100] rev 8269
remove *.out;
oheimb [Mon, 21 Feb 2000 13:57:07 +0100] rev 8268
renamed Univalent to univalent
paulson [Mon, 21 Feb 2000 11:16:19 +0100] rev 8267
simplified some proofs
paulson [Mon, 21 Feb 2000 11:15:43 +0100] rev 8266
new examples that cannot be done in LEO
nipkow [Mon, 21 Feb 2000 10:20:38 +0100] rev 8265
A few lemmas and some Adds.
nipkow [Sun, 20 Feb 2000 09:32:06 +0100] rev 8264
Added global let-simplification rule.
nipkow [Sat, 19 Feb 2000 13:47:12 +0100] rev 8263
Commenst.
oheimb [Fri, 18 Feb 2000 20:27:19 +0100] rev 8262
added instance declaration for finite product
oheimb [Fri, 18 Feb 2000 20:25:29 +0100] rev 8261
added split_eta_SetCompr, SetCompr_Sigma_eq
oheimb [Fri, 18 Feb 2000 20:24:56 +0100] rev 8260
added Suc_le_D
oheimb [Fri, 18 Feb 2000 20:24:40 +0100] rev 8259
added domI, domD
oheimb [Fri, 18 Feb 2000 20:24:16 +0100] rev 8258
changed precedence of function update
nipkow [Fri, 18 Feb 2000 18:29:28 +0100] rev 8257
installed lin arith for nat numerals.
paulson [Fri, 18 Feb 2000 15:37:08 +0100] rev 8256
Rename: theory for applying a bijection over states to a UNITY program
paulson [Fri, 18 Feb 2000 15:35:29 +0100] rev 8255
new distributive laws
paulson [Fri, 18 Feb 2000 15:34:22 +0100] rev 8254
expandshort
paulson [Fri, 18 Feb 2000 15:33:09 +0100] rev 8253
many new theorems about inj, surj etc.
paulson [Fri, 18 Feb 2000 15:28:32 +0100] rev 8252
new theorem nat_diff_split'
paulson [Fri, 18 Feb 2000 15:20:44 +0100] rev 8251
New treatment of "guarantees" with polymorphic components and bijections.
Works EXCEPT FOR Alloc.
wenzelm [Wed, 16 Feb 2000 15:04:12 +0100] rev 8250
Syntax translation functions;
paulson [Wed, 16 Feb 2000 10:51:23 +0100] rev 8249
fixed some overfull lines
paulson [Wed, 16 Feb 2000 10:50:57 +0100] rev 8248
a smaller point size reduces the number of overfull figures
kleing [Tue, 15 Feb 2000 21:02:55 +0100] rev 8247
cosmetics
wenzelm [Tue, 15 Feb 2000 19:41:44 +0100] rev 8246
fixed sel_upd simproc (less efficient, but more complete);
kleing [Tue, 15 Feb 2000 17:51:11 +0100] rev 8245
lightweight bytecode verifier with correctness proof
wenzelm [Mon, 14 Feb 2000 20:49:08 +0100] rev 8244
basic source deps;
wenzelm [Mon, 14 Feb 2000 20:43:12 +0100] rev 8243
easy_setup: fixed mksimps;
wenzelm [Mon, 14 Feb 2000 20:42:02 +0100] rev 8242
proof step: reset goal_facts;
wenzelm [Mon, 14 Feb 2000 12:23:08 +0100] rev 8241
mkdir -p $ISABELLE_BROWSER_INFO;
wenzelm [Mon, 14 Feb 2000 11:23:57 +0100] rev 8240
fixed prefer;
wenzelm [Mon, 14 Feb 2000 11:23:44 +0100] rev 8239
tuned msg;
wenzelm [Sun, 13 Feb 2000 21:01:26 +0100] rev 8238
added refine_end;
res_inst tactic emulation;
wenzelm [Sun, 13 Feb 2000 21:00:02 +0100] rev 8237
tuned attrib;
wenzelm [Sun, 13 Feb 2000 20:58:13 +0100] rev 8236
apply: observe facts;
apply_end;
wenzelm [Sun, 13 Feb 2000 20:56:55 +0100] rev 8235
prf_script commands made proper;
removed then_apply;
added apply_end;
wenzelm [Sun, 13 Feb 2000 20:54:12 +0100] rev 8234
refine_end;
wenzelm [Sun, 13 Feb 2000 20:52:58 +0100] rev 8233
attrib: keyword_symid;
goal_spec;
wenzelm [Thu, 10 Feb 2000 20:54:40 +0100] rev 8232
\isabellesimplestyle;
wenzelm [Thu, 10 Feb 2000 20:54:18 +0100] rev 8231
symid: include single symbolic char;
wenzelm [Thu, 10 Feb 2000 20:52:59 +0100] rev 8230
is_symbolic;
wenzelm [Thu, 10 Feb 2000 13:36:23 +0100] rev 8229
theorems [elim??] = sym;
wenzelm [Thu, 10 Feb 2000 13:34:52 +0100] rev 8228
added easy_setup;
wenzelm [Thu, 10 Feb 2000 13:34:38 +0100] rev 8227
add_judgment;
paulson [Thu, 10 Feb 2000 11:08:42 +0100] rev 8226
new thm and simprule inv_id
paulson [Thu, 10 Feb 2000 11:03:54 +0100] rev 8225
Cambridge-specific modifications
wenzelm [Wed, 09 Feb 2000 14:35:23 +0100] rev 8224
mirror dist page;
wenzelm [Wed, 09 Feb 2000 14:12:14 +0100] rev 8223
tuned;
wenzelm [Wed, 09 Feb 2000 14:03:29 +0100] rev 8222
mirror main page;
kleing [Wed, 09 Feb 2000 13:43:35 +0100] rev 8221
clearer "Obtaining" section
wenzelm [Wed, 09 Feb 2000 12:30:25 +0100] rev 8220
[df]rule methods;
wenzelm [Wed, 09 Feb 2000 12:30:04 +0100] rev 8219
document -c;
wenzelm [Wed, 09 Feb 2000 12:29:03 +0100] rev 8218
eliminated gif dir;
wenzelm [Wed, 09 Feb 2000 12:28:44 +0100] rev 8217
option -c;
paulson [Wed, 09 Feb 2000 11:45:10 +0100] rev 8216
updated the Client example
paulson [Wed, 09 Feb 2000 11:43:53 +0100] rev 8215
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson [Wed, 09 Feb 2000 11:42:26 +0100] rev 8214
new thm order_less_imp_le
wenzelm [Tue, 08 Feb 2000 22:28:30 +0100] rev 8213
(then_)tac: assert_backward;
wenzelm [Tue, 08 Feb 2000 20:17:41 +0100] rev 8212
added -c option (beware!);
changed default DIR to 'document';
NOTE: please ignore last log entry;
wenzelm [Tue, 08 Feb 2000 20:14:58 +0100] rev 8211
rename -p to -P;
fixed target name: LOGIC-NAME;
wenzelm [Tue, 08 Feb 2000 20:14:09 +0100] rev 8210
added forget_proof;
wenzelm [Tue, 08 Feb 2000 20:13:58 +0100] rev 8209
added K.qed_global;
wenzelm [Tue, 08 Feb 2000 20:12:36 +0100] rev 8208
omit Primes;
wenzelm [Mon, 07 Feb 2000 18:42:47 +0100] rev 8207
(then_)apply: prove -> prove;
wenzelm [Mon, 07 Feb 2000 18:40:40 +0100] rev 8206
assert_no_chain;
wenzelm [Mon, 07 Feb 2000 18:40:27 +0100] rev 8205
refine_no_facts: recover goal_facts;
wenzelm [Mon, 07 Feb 2000 18:39:53 +0100] rev 8204
tuned prefer/defer;
wenzelm [Mon, 07 Feb 2000 18:38:51 +0100] rev 8203
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
oheimb [Mon, 07 Feb 2000 15:28:43 +0100] rev 8202
paper available
paulson [Mon, 07 Feb 2000 15:14:02 +0100] rev 8201
tidied some proofs
kleing [Sat, 05 Feb 2000 17:31:53 +0100] rev 8200
Branch: top elements of stack only need to be convertible (not equal)
wenzelm [Sat, 05 Feb 2000 17:06:27 +0100] rev 8199
tuned;
wenzelm [Sat, 05 Feb 2000 16:59:50 +0100] rev 8198
-I option;
wenzelm [Sat, 05 Feb 2000 16:58:58 +0100] rev 8197
-D PATH: dump generated document sources into PATH;
wenzelm [Sat, 05 Feb 2000 16:57:02 +0100] rev 8196
additional tex dump;
wenzelm [Sat, 05 Feb 2000 16:54:27 +0100] rev 8195
'.' == by this;
wenzelm [Fri, 04 Feb 2000 21:53:36 +0100] rev 8194
misc improvements;
wenzelm [Fri, 04 Feb 2000 21:45:57 +0100] rev 8193
added MicroJava/document;
wenzelm [Fri, 04 Feb 2000 21:44:38 +0100] rev 8192
added old_symbol_source;
tuned;
wenzelm [Fri, 04 Feb 2000 21:44:04 +0100] rev 8191
Present.old_symbol_source;
wenzelm [Fri, 04 Feb 2000 21:43:30 +0100] rev 8190
tuned;
wenzelm [Fri, 04 Feb 2000 21:37:23 +0100] rev 8189
manually load session;
wenzelm [Fri, 04 Feb 2000 21:36:13 +0100] rev 8188
tuned syms;
paulson [Fri, 04 Feb 2000 11:36:11 +0100] rev 8187
new theorem gcd_add_mult
wenzelm [Wed, 02 Feb 2000 20:19:25 +0100] rev 8186
most_general_varify_tfrees all results;
nipkow [Wed, 02 Feb 2000 13:26:38 +0100] rev 8185
Rduced Class C <= Class D to C <= D.