Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fri, 14 Jul 2000 16:27:45 +0200 added hint on fun_sum
changeset
oheimb [Fri, 14 Jul 2000 16:27:45 +0200] rev 9340
added hint on fun_sum
Fri, 14 Jul 2000 16:27:42 +0200 added fun_upd2_simproc
changeset
oheimb [Fri, 14 Jul 2000 16:27:42 +0200] rev 9339
added fun_upd2_simproc
Fri, 14 Jul 2000 16:27:37 +0200 re-added subset_empty to simpset
changeset
oheimb [Fri, 14 Jul 2000 16:27:37 +0200] rev 9338
re-added subset_empty to simpset
Fri, 14 Jul 2000 14:51:02 +0200 used bounded quantification in definition of guarantees and other minor
changeset
paulson [Fri, 14 Jul 2000 14:51:02 +0200] rev 9337
used bounded quantification in definition of guarantees and other minor adjustments
Fri, 14 Jul 2000 14:47:15 +0200 moved sublist from UNITY/AllocBase to List
changeset
paulson [Fri, 14 Jul 2000 14:47:15 +0200] rev 9336
moved sublist from UNITY/AllocBase to List
Fri, 14 Jul 2000 14:46:35 +0200 AddIffs
changeset
paulson [Fri, 14 Jul 2000 14:46:35 +0200] rev 9335
AddIffs
Fri, 14 Jul 2000 13:57:00 +0200 parent should be Main
changeset
paulson [Fri, 14 Jul 2000 13:57:00 +0200] rev 9334
parent should be Main
Fri, 14 Jul 2000 13:39:03 +0200 changed the quotient syntax from / to //
changeset
paulson [Fri, 14 Jul 2000 13:39:03 +0200] rev 9333
changed the quotient syntax from / to //
Thu, 13 Jul 2000 23:26:08 +0200 tuned cycle_msg;
changeset
wenzelm [Thu, 13 Jul 2000 23:26:08 +0200] rev 9332
tuned cycle_msg;
Thu, 13 Jul 2000 23:23:24 +0200 updated;
changeset
wenzelm [Thu, 13 Jul 2000 23:23:24 +0200] rev 9331
updated;
Thu, 13 Jul 2000 23:22:26 +0200 HOL: the disjoint sum is now "<+>" instead of "Plus";
changeset
wenzelm [Thu, 13 Jul 2000 23:22:26 +0200] rev 9330
HOL: the disjoint sum is now "<+>" instead of "Plus"; ML: PureThy.add_defs gets additional argument;
Thu, 13 Jul 2000 23:20:57 +0200 adapted PureThy.add_defs_i;
changeset
wenzelm [Thu, 13 Jul 2000 23:20:57 +0200] rev 9329
adapted PureThy.add_defs_i;
Thu, 13 Jul 2000 23:20:33 +0200 defs (overloaded);
changeset
wenzelm [Thu, 13 Jul 2000 23:20:33 +0200] rev 9328
defs (overloaded);
Thu, 13 Jul 2000 23:20:14 +0200 tuned;
changeset
wenzelm [Thu, 13 Jul 2000 23:20:14 +0200] rev 9327
tuned;
Thu, 13 Jul 2000 23:19:40 +0200 added read_xnum;
changeset
wenzelm [Thu, 13 Jul 2000 23:19:40 +0200] rev 9326
added read_xnum;
Thu, 13 Jul 2000 23:19:08 +0200 fix(_i): admit internal variables;
changeset
wenzelm [Thu, 13 Jul 2000 23:19:08 +0200] rev 9325
fix(_i): admit internal variables;
Thu, 13 Jul 2000 23:18:36 +0200 use ProofContext.bind_skolem;
changeset
wenzelm [Thu, 13 Jul 2000 23:18:36 +0200] rev 9324
use ProofContext.bind_skolem;
Thu, 13 Jul 2000 23:17:44 +0200 defs: (overloaded) option;
changeset
wenzelm [Thu, 13 Jul 2000 23:17:44 +0200] rev 9323
defs: (overloaded) option;
Thu, 13 Jul 2000 23:17:14 +0200 eq_prop: strip_assums_concl;
changeset
wenzelm [Thu, 13 Jul 2000 23:17:14 +0200] rev 9322
eq_prop: strip_assums_concl;
Thu, 13 Jul 2000 23:16:48 +0200 tuned exceptions;
changeset
wenzelm [Thu, 13 Jul 2000 23:16:48 +0200] rev 9321
tuned exceptions; added add_deps_acyclic, merge_acyclic;
Thu, 13 Jul 2000 23:16:13 +0200 const_deps: unit Graph.T;
changeset
wenzelm [Thu, 13 Jul 2000 23:16:13 +0200] rev 9320
const_deps: unit Graph.T; proper merge of const_deps; tuned;
Thu, 13 Jul 2000 23:15:20 +0200 add_term_consts: ins_string;
changeset
wenzelm [Thu, 13 Jul 2000 23:15:20 +0200] rev 9319
add_term_consts: ins_string;
Thu, 13 Jul 2000 23:14:49 +0200 add_defs(_i): overloaded option;
changeset
wenzelm [Thu, 13 Jul 2000 23:14:49 +0200] rev 9318
add_defs(_i): overloaded option;
Thu, 13 Jul 2000 23:14:15 +0200 adapted PureThy.add_defs;
changeset
wenzelm [Thu, 13 Jul 2000 23:14:15 +0200] rev 9317
adapted PureThy.add_defs;
Thu, 13 Jul 2000 23:13:52 +0200 fixed comment;
changeset
wenzelm [Thu, 13 Jul 2000 23:13:52 +0200] rev 9316
fixed comment;
Thu, 13 Jul 2000 23:13:10 +0200 adapted PureThy.add_defs_i;
changeset
wenzelm [Thu, 13 Jul 2000 23:13:10 +0200] rev 9315
adapted PureThy.add_defs_i;
Thu, 13 Jul 2000 23:11:38 +0200 use Syntax.read_xnum;
changeset
wenzelm [Thu, 13 Jul 2000 23:11:38 +0200] rev 9314
use Syntax.read_xnum;
Thu, 13 Jul 2000 23:11:14 +0200 fixed simplified_cases;
changeset
wenzelm [Thu, 13 Jul 2000 23:11:14 +0200] rev 9313
fixed simplified_cases;
Thu, 13 Jul 2000 23:10:12 +0200 fixed name: UN_empty3;
changeset
wenzelm [Thu, 13 Jul 2000 23:10:12 +0200] rev 9312
fixed name: UN_empty3;
Thu, 13 Jul 2000 23:09:25 +0200 replaced infix Plus by <+>;
changeset
wenzelm [Thu, 13 Jul 2000 23:09:25 +0200] rev 9311
replaced infix Plus by <+>;
Thu, 13 Jul 2000 23:09:03 +0200 removed duplicate Compl_atMost;
changeset
wenzelm [Thu, 13 Jul 2000 23:09:03 +0200] rev 9310
removed duplicate Compl_atMost;
Thu, 13 Jul 2000 23:08:42 +0200 fixed compose decl;
changeset
wenzelm [Thu, 13 Jul 2000 23:08:42 +0200] rev 9309
fixed compose decl;
Thu, 13 Jul 2000 23:08:20 +0200 defs: (overloaded) option;
changeset
wenzelm [Thu, 13 Jul 2000 23:08:20 +0200] rev 9308
defs: (overloaded) option;
Thu, 13 Jul 2000 23:07:56 +0200 method cases/induct: (opaque) option;
changeset
wenzelm [Thu, 13 Jul 2000 23:07:56 +0200] rev 9307
method cases/induct: (opaque) option;
Thu, 13 Jul 2000 23:07:10 +0200 defs (overloaded);
changeset
wenzelm [Thu, 13 Jul 2000 23:07:10 +0200] rev 9306
defs (overloaded);
Thu, 13 Jul 2000 13:05:58 +0200 removed now-redundant proof steps
changeset
paulson [Thu, 13 Jul 2000 13:05:58 +0200] rev 9305
removed now-redundant proof steps
Thu, 13 Jul 2000 13:04:48 +0200 added an important default rule
changeset
paulson [Thu, 13 Jul 2000 13:04:48 +0200] rev 9304
added an important default rule
Thu, 13 Jul 2000 13:02:20 +0200 fixed a failing proof
changeset
paulson [Thu, 13 Jul 2000 13:02:20 +0200] rev 9303
fixed a failing proof
Thu, 13 Jul 2000 13:00:22 +0200 le_refl_iff as default rule
changeset
paulson [Thu, 13 Jul 2000 13:00:22 +0200] rev 9302
le_refl_iff as default rule
Thu, 13 Jul 2000 12:59:26 +0200 removed needless premises
changeset
paulson [Thu, 13 Jul 2000 12:59:26 +0200] rev 9301
removed needless premises
Thu, 13 Jul 2000 12:56:42 +0200 AddIffs now available for FOL, ZF
changeset
paulson [Thu, 13 Jul 2000 12:56:42 +0200] rev 9300
AddIffs now available for FOL, ZF
Thu, 13 Jul 2000 11:44:02 +0200 added simp_case_tac;
changeset
wenzelm [Thu, 13 Jul 2000 11:44:02 +0200] rev 9299
added simp_case_tac; proper handling of case names with simplification; support "(opaque)" mode; tuned;
Thu, 13 Jul 2000 11:42:11 +0200 use InductMethod.simp_case_tac;
changeset
wenzelm [Thu, 13 Jul 2000 11:42:11 +0200] rev 9298
use InductMethod.simp_case_tac;
Thu, 13 Jul 2000 11:41:40 +0200 tuned;
changeset
wenzelm [Thu, 13 Jul 2000 11:41:40 +0200] rev 9297
tuned;
Thu, 13 Jul 2000 11:41:06 +0200 export thesisN separately;
changeset
wenzelm [Thu, 13 Jul 2000 11:41:06 +0200] rev 9296
export thesisN separately;
Thu, 13 Jul 2000 11:40:49 +0200 prep rhs in original context;
changeset
wenzelm [Thu, 13 Jul 2000 11:40:49 +0200] rev 9295
prep rhs in original context; tuned;
Thu, 13 Jul 2000 11:39:41 +0200 RuleCases.make opaq;
changeset
wenzelm [Thu, 13 Jul 2000 11:39:41 +0200] rev 9294
RuleCases.make opaq;
Thu, 13 Jul 2000 11:39:22 +0200 bind_skolem;
changeset
wenzelm [Thu, 13 Jul 2000 11:39:22 +0200] rev 9293
bind_skolem;
Thu, 13 Jul 2000 11:39:03 +0200 invoke_case: bind_skolem;
changeset
wenzelm [Thu, 13 Jul 2000 11:39:03 +0200] rev 9292
invoke_case: bind_skolem;
Thu, 13 Jul 2000 11:38:42 +0200 "_i" arguments now expected to have skolems already internalized;
changeset
wenzelm [Thu, 13 Jul 2000 11:38:42 +0200] rev 9291
"_i" arguments now expected to have skolems already internalized; removed unused cert_skolem, export intern_skolem, added bind_skolem;
Thu, 13 Jul 2000 11:36:57 +0200 make: opaq flag;
changeset
wenzelm [Thu, 13 Jul 2000 11:36:57 +0200] rev 9290
make: opaq flag;
Thu, 13 Jul 2000 11:36:29 +0200 added internal, dest_internal;
changeset
wenzelm [Thu, 13 Jul 2000 11:36:29 +0200] rev 9289
added internal, dest_internal;
Wed, 12 Jul 2000 16:44:34 +0200 infix 'OF' is a version of 'MRS' with more appropriate argument order;
changeset
wenzelm [Wed, 12 Jul 2000 16:44:34 +0200] rev 9288
infix 'OF' is a version of 'MRS' with more appropriate argument order;
Wed, 12 Jul 2000 14:47:55 +0200 about.html -> logics.html
changeset
kleing [Wed, 12 Jul 2000 14:47:55 +0200] rev 9287
about.html -> logics.html
Wed, 12 Jul 2000 14:47:34 +0200 munich webserver is now sunbroy51
changeset
kleing [Wed, 12 Jul 2000 14:47:34 +0200] rev 9286
munich webserver is now sunbroy51
Wed, 12 Jul 2000 14:46:28 +0200 about -> logics, better access to online libraries
changeset
kleing [Wed, 12 Jul 2000 14:46:28 +0200] rev 9285
about -> logics, better access to online libraries
Mon, 10 Jul 2000 12:17:34 +0200 removal of (harmless) circular definitions
changeset
paulson [Mon, 10 Jul 2000 12:17:34 +0200] rev 9284
removal of (harmless) circular definitions
Sun, 09 Jul 2000 16:01:42 +0200 Tuned proof.
changeset
berghofe [Sun, 09 Jul 2000 16:01:42 +0200] rev 9283
Tuned proof.
Sat, 08 Jul 2000 19:14:43 +0200 Defs are now checked for circularity (if not overloaded).
changeset
nipkow [Sat, 08 Jul 2000 19:14:43 +0200] rev 9282
Defs are now checked for circularity (if not overloaded).
Fri, 07 Jul 2000 21:51:52 +0200 inter_sort: keep normal!
changeset
wenzelm [Fri, 07 Jul 2000 21:51:52 +0200] rev 9281
inter_sort: keep normal!
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle