wenzelm [Fri, 26 Jul 2019 09:59:11 +0200] rev 70415
finalize proofs earlier to reduce memory requirement;
wenzelm [Fri, 26 Jul 2019 09:50:23 +0200] rev 70414
proper proof_serial;
wenzelm [Fri, 26 Jul 2019 09:50:12 +0200] rev 70413
more explicit type proof_serial;
wenzelm [Fri, 26 Jul 2019 09:35:02 +0200] rev 70412
defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement;
misc tuning and clarification;
wenzelm [Thu, 25 Jul 2019 14:01:06 +0200] rev 70411
more accurate proof definitions (PThm nodes);
wenzelm [Wed, 24 Jul 2019 15:41:24 +0200] rev 70410
avoid duplicate Thm.name_derivation on unnamed PThm nodes ("simps" vs. "case_eqns" and "recursor_eqns");
wenzelm [Wed, 24 Jul 2019 13:30:15 +0200] rev 70409
prefer local counter;
wenzelm [Wed, 24 Jul 2019 13:19:00 +0200] rev 70408
more accurate proof export;
wenzelm [Wed, 24 Jul 2019 13:18:15 +0200] rev 70407
clarified syntax;
wenzelm [Wed, 24 Jul 2019 11:57:30 +0200] rev 70406
tuned;
wenzelm [Wed, 24 Jul 2019 11:54:08 +0200] rev 70405
more thorough clean_proof;
wenzelm [Wed, 24 Jul 2019 11:32:18 +0200] rev 70404
clarified modules;
wenzelm [Wed, 24 Jul 2019 10:49:01 +0200] rev 70403
avoid global syntax for MinProof (amending e31271559de8);
wenzelm [Tue, 23 Jul 2019 23:10:22 +0200] rev 70402
treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);
wenzelm [Tue, 23 Jul 2019 19:07:28 +0200] rev 70401
discontinued Proofterm.Promise (cf. 725438ceae7c);
wenzelm [Tue, 23 Jul 2019 19:04:56 +0200] rev 70400
clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named;
added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof;
wenzelm [Tue, 23 Jul 2019 12:16:02 +0200] rev 70399
tuned comments;
wenzelm [Tue, 23 Jul 2019 12:07:50 +0200] rev 70398
proof terms are always constructed sequentially;
discontinued unused Proofterm.Promise -- too complex;
wenzelm [Mon, 22 Jul 2019 21:55:02 +0200] rev 70397
tuned comments -- proper sections;
wenzelm [Mon, 22 Jul 2019 16:15:40 +0200] rev 70396
support export_proofs, prune_proofs;
tuned comments;
wenzelm [Mon, 22 Jul 2019 14:47:21 +0200] rev 70395
clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;
wenzelm [Mon, 22 Jul 2019 11:40:04 +0200] rev 70394
tuned;
wenzelm [Mon, 22 Jul 2019 11:39:30 +0200] rev 70393
clarified exception;
wenzelm [Mon, 22 Jul 2019 11:31:42 +0200] rev 70392
tuned;
wenzelm [Mon, 22 Jul 2019 11:10:08 +0200] rev 70391
more accurate type information;
wenzelm [Mon, 22 Jul 2019 11:09:24 +0200] rev 70390
unused (see also 42fbb6abed5a);
wenzelm [Sun, 21 Jul 2019 15:42:43 +0200] rev 70389
discontinued ASCII syntax;
wenzelm [Sun, 21 Jul 2019 15:19:07 +0200] rev 70388
global declaration of abstract syntax for proof terms, with qualified names;
clarified modules;
wenzelm [Sun, 21 Jul 2019 12:28:02 +0200] rev 70387
tuned;
wenzelm [Sun, 21 Jul 2019 12:11:35 +0200] rev 70386
tuned;
wenzelm [Sat, 20 Jul 2019 14:03:51 +0200] rev 70385
more operations: support type classes within the logic;
wenzelm [Sat, 20 Jul 2019 12:52:29 +0200] rev 70384
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm [Sat, 20 Jul 2019 11:48:30 +0200] rev 70383
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm [Sat, 20 Jul 2019 11:17:54 +0200] rev 70382
more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
paulson <lp15@cam.ac.uk> [Fri, 19 Jul 2019 12:57:14 +0100] rev 70381
More results about measure and integration theory
paulson <lp15@cam.ac.uk> [Thu, 18 Jul 2019 15:40:15 +0100] rev 70380
More analysis / measure theory material
paulson [Thu, 18 Jul 2019 14:08:44 +0100] rev 70379
merged
paulson <lp15@cam.ac.uk> [Thu, 18 Jul 2019 14:08:28 +0100] rev 70378
more new material about analysis
nipkow [Thu, 18 Jul 2019 12:06:42 +0200] rev 70377
added forgotten declaration provided by Florian Haftmann
wenzelm [Wed, 17 Jul 2019 22:24:20 +0200] rev 70376
merged;
wenzelm [Wed, 17 Jul 2019 21:56:32 +0200] rev 70375
updated to jedit_build-20190717: support more brackets;
wenzelm [Wed, 17 Jul 2019 21:32:03 +0200] rev 70374
updated to isabelle_fonts-20190717;
wenzelm [Wed, 17 Jul 2019 17:12:57 +0200] rev 70373
redundant;
wenzelm [Wed, 17 Jul 2019 17:03:50 +0200] rev 70372
tuned;
wenzelm [Wed, 17 Jul 2019 16:10:05 +0200] rev 70371
added \<llangle>, \<rrangle>;
discontinued special rendering for old {* *};
wenzelm [Wed, 17 Jul 2019 11:18:39 +0200] rev 70370
tuned doc isar-ref;
wenzelm [Wed, 17 Jul 2019 11:09:43 +0200] rev 70369
added \<bbar>;
wenzelm [Wed, 17 Jul 2019 09:40:43 +0200] rev 70368
added \<sqdot>;
paulson <lp15@cam.ac.uk> [Wed, 17 Jul 2019 16:32:06 +0100] rev 70367
fixed renaming issues
paulson [Wed, 17 Jul 2019 14:02:50 +0100] rev 70366
merged
paulson <lp15@cam.ac.uk> [Wed, 17 Jul 2019 14:02:42 +0100] rev 70365
a few new lemmas and a bit of tidying
wenzelm [Tue, 16 Jul 2019 15:39:32 +0200] rev 70364
support for a soft-type system within the Isabelle logical framework;
nipkow [Thu, 11 Jul 2019 18:37:52 +0200] rev 70363
tuned
wenzelm [Thu, 04 Jul 2019 14:20:47 +0200] rev 70362
proper theory naming after join (reset due to merge_data);
wenzelm [Thu, 04 Jul 2019 12:31:24 +0200] rev 70361
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm [Thu, 04 Jul 2019 11:26:00 +0200] rev 70360
clarified history stage: allow independent updates that are merged later;