Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sat, 30 Oct 2021 13:26:33 +0200 tuned;
changeset
wenzelm [Sat, 30 Oct 2021 13:26:33 +0200] rev 74638
tuned;
Sat, 30 Oct 2021 13:12:22 +0200 test version of prespective polyml-5.9;
changeset
wenzelm [Sat, 30 Oct 2021 13:12:22 +0200] rev 74637
test version of prespective polyml-5.9;
Sat, 30 Oct 2021 12:26:56 +0200 clarified antiquotations;
changeset
wenzelm [Sat, 30 Oct 2021 12:26:56 +0200] rev 74636
clarified antiquotations;
Sat, 30 Oct 2021 12:03:43 +0200 updated for pre-5.9 testing;
changeset
wenzelm [Sat, 30 Oct 2021 12:03:43 +0200] rev 74635
updated for pre-5.9 testing;
Sat, 30 Oct 2021 11:59:41 +0200 clarified antiquotations;
changeset
wenzelm [Sat, 30 Oct 2021 11:59:41 +0200] rev 74634
clarified antiquotations;
Sat, 30 Oct 2021 11:59:23 +0200 clarified antiquotations;
changeset
wenzelm [Sat, 30 Oct 2021 11:59:23 +0200] rev 74633
clarified antiquotations;
Fri, 29 Oct 2021 21:06:08 +0200 clarified antiquotations;
changeset
wenzelm [Fri, 29 Oct 2021 21:06:08 +0200] rev 74632
clarified antiquotations;
Fri, 29 Oct 2021 20:39:16 +0200 more robust subgoal addressing;
changeset
wenzelm [Fri, 29 Oct 2021 20:39:16 +0200] rev 74631
more robust subgoal addressing;
Fri, 29 Oct 2021 20:15:59 +0200 proper subgoal addressing;
changeset
wenzelm [Fri, 29 Oct 2021 20:15:59 +0200] rev 74630
proper subgoal addressing;
Fri, 29 Oct 2021 20:04:33 +0200 clarified antiquotations;
changeset
wenzelm [Fri, 29 Oct 2021 20:04:33 +0200] rev 74629
clarified antiquotations;
Fri, 29 Oct 2021 19:49:11 +0200 recursive find_eq, not find_dist;
changeset
wenzelm [Fri, 29 Oct 2021 19:49:11 +0200] rev 74628
recursive find_eq, not find_dist;
Fri, 29 Oct 2021 19:43:32 +0200 misc tuning and clarification;
changeset
wenzelm [Fri, 29 Oct 2021 19:43:32 +0200] rev 74627
misc tuning and clarification;
Fri, 29 Oct 2021 19:17:24 +0200 clarified antiquotations;
changeset
wenzelm [Fri, 29 Oct 2021 19:17:24 +0200] rev 74626
clarified antiquotations;
Fri, 29 Oct 2021 15:09:46 +0200 order_tac: prevent potential bug, improve perf and tracing
changeset
Lukas Stevens <mail@lukas-stevens.de> [Fri, 29 Oct 2021 15:09:46 +0200] rev 74625
order_tac: prevent potential bug, improve perf and tracing - We need to be careful when the order operators contain schematic variables, e.g. <= = ccw' ?p.
Fri, 29 Oct 2021 13:23:41 +0200 misc tuning and clarification;
changeset
wenzelm [Fri, 29 Oct 2021 13:23:41 +0200] rev 74624
misc tuning and clarification;
Fri, 29 Oct 2021 13:04:51 +0200 clarified antiquotations;
changeset
wenzelm [Fri, 29 Oct 2021 13:04:51 +0200] rev 74623
clarified antiquotations;
Fri, 29 Oct 2021 12:42:06 +0200 clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
changeset
wenzelm [Fri, 29 Oct 2021 12:42:06 +0200] rev 74622
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
Fri, 29 Oct 2021 12:30:47 +0200 clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
changeset
wenzelm [Fri, 29 Oct 2021 12:30:47 +0200] rev 74621
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
Fri, 29 Oct 2021 11:59:02 +0200 avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);
changeset
wenzelm [Fri, 29 Oct 2021 11:59:02 +0200] rev 74620
avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);
Fri, 29 Oct 2021 11:57:49 +0200 added Thm.instantiate_beta;
changeset
wenzelm [Fri, 29 Oct 2021 11:57:49 +0200] rev 74619
added Thm.instantiate_beta; tuned;
Thu, 28 Oct 2021 06:39:36 +0000 moved generic implementation into HOL-Main
changeset
haftmann [Thu, 28 Oct 2021 06:39:36 +0000] rev 74618
moved generic implementation into HOL-Main
Fri, 29 Oct 2021 00:01:14 +0200 tuned;
changeset
wenzelm [Fri, 29 Oct 2021 00:01:14 +0200] rev 74617
tuned;
Thu, 28 Oct 2021 23:44:31 +0200 tuned;
changeset
wenzelm [Thu, 28 Oct 2021 23:44:31 +0200] rev 74616
tuned;
Thu, 28 Oct 2021 23:37:53 +0200 clarified antiquotations;
changeset
wenzelm [Thu, 28 Oct 2021 23:37:53 +0200] rev 74615
clarified antiquotations;
Thu, 28 Oct 2021 21:28:52 +0200 clarified antiquotations;
changeset
wenzelm [Thu, 28 Oct 2021 21:28:52 +0200] rev 74614
clarified antiquotations;
Thu, 28 Oct 2021 20:38:21 +0200 discontinued somewhat pointless antiquotations;
changeset
wenzelm [Thu, 28 Oct 2021 20:38:21 +0200] rev 74613
discontinued somewhat pointless antiquotations;
Thu, 28 Oct 2021 20:32:40 +0200 NEWS;
changeset
wenzelm [Thu, 28 Oct 2021 20:32:40 +0200] rev 74612
NEWS;
Thu, 28 Oct 2021 20:09:37 +0200 clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;
changeset
wenzelm [Thu, 28 Oct 2021 20:09:37 +0200] rev 74611
clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;
Thu, 28 Oct 2021 20:06:29 +0200 clarified antiquotations;
changeset
wenzelm [Thu, 28 Oct 2021 20:06:29 +0200] rev 74610
clarified antiquotations;
Thu, 28 Oct 2021 20:05:18 +0200 clarified antiquotations;
changeset
wenzelm [Thu, 28 Oct 2021 20:05:18 +0200] rev 74609
clarified antiquotations;
Thu, 28 Oct 2021 20:04:06 +0200 clarified antiquotations;
changeset
wenzelm [Thu, 28 Oct 2021 20:04:06 +0200] rev 74608
clarified antiquotations;
Thu, 28 Oct 2021 20:01:59 +0200 clarified antiquotations;
changeset
wenzelm [Thu, 28 Oct 2021 20:01:59 +0200] rev 74607
clarified antiquotations;
Thu, 28 Oct 2021 18:37:33 +0200 support for "lemma";
changeset
wenzelm [Thu, 28 Oct 2021 18:37:33 +0200] rev 74606
support for "lemma"; support for "schematic" mode; clarified error position;
Thu, 28 Oct 2021 13:20:45 +0200 tuned;
changeset
wenzelm [Thu, 28 Oct 2021 13:20:45 +0200] rev 74605
tuned;
Thu, 28 Oct 2021 13:13:48 +0200 local fixes for "lemma" antiquotation;
changeset
wenzelm [Thu, 28 Oct 2021 13:13:48 +0200] rev 74604
local fixes for "lemma" antiquotation;
Thu, 28 Oct 2021 12:25:47 +0200 clarified signature;
changeset
wenzelm [Thu, 28 Oct 2021 12:25:47 +0200] rev 74603
clarified signature;
Thu, 28 Oct 2021 12:14:53 +0200 tuned;
changeset
wenzelm [Thu, 28 Oct 2021 12:14:53 +0200] rev 74602
tuned;
Thu, 28 Oct 2021 12:09:58 +0200 clarified keywords: major take precedence for commands, but not used for antiquotations;
changeset
wenzelm [Thu, 28 Oct 2021 12:09:58 +0200] rev 74601
clarified keywords: major take precedence for commands, but not used for antiquotations; clarified modules;
Thu, 28 Oct 2021 11:37:49 +0200 tuned modules;
changeset
wenzelm [Thu, 28 Oct 2021 11:37:49 +0200] rev 74600
tuned modules;
Wed, 27 Oct 2021 20:07:13 +0200 more antiquotations;
changeset
wenzelm [Wed, 27 Oct 2021 20:07:13 +0200] rev 74599
more antiquotations;
Wed, 27 Oct 2021 11:47:42 +0100 moved a theorem to a sensible place
changeset
paulson <lp15@cam.ac.uk> [Wed, 27 Oct 2021 11:47:42 +0100] rev 74598
moved a theorem to a sensible place
Tue, 26 Oct 2021 22:58:20 +0200 merged
changeset
wenzelm [Tue, 26 Oct 2021 22:58:20 +0200] rev 74597
merged
Tue, 26 Oct 2021 22:26:47 +0200 tuned, continuing e955964d89cb;
changeset
wenzelm [Tue, 26 Oct 2021 22:26:47 +0200] rev 74596
tuned, continuing e955964d89cb;
Tue, 26 Oct 2021 22:04:33 +0200 avoid waste of resources due to dynamic simpset (amending 45c09620f726);
changeset
wenzelm [Tue, 26 Oct 2021 22:04:33 +0200] rev 74595
avoid waste of resources due to dynamic simpset (amending 45c09620f726);
Tue, 26 Oct 2021 17:14:16 +0200 fix latex
changeset
Norbert Schirmer <nschirmer@apple.com> [Tue, 26 Oct 2021 17:14:16 +0200] rev 74594
fix latex
Tue, 26 Oct 2021 16:01:05 +0200 clarified modules;
changeset
wenzelm [Tue, 26 Oct 2021 16:01:05 +0200] rev 74593
clarified modules;
Tue, 26 Oct 2021 14:43:59 +0000 more generic bit/word lemmas for distribution
changeset
haftmann [Tue, 26 Oct 2021 14:43:59 +0000] rev 74592
more generic bit/word lemmas for distribution
Tue, 26 Oct 2021 16:22:03 +0100 merged
changeset
paulson [Tue, 26 Oct 2021 16:22:03 +0100] rev 74591
merged
Tue, 26 Oct 2021 11:15:40 +0100 Added / moved some simple set-theoretic lemmas
changeset
paulson <lp15@cam.ac.uk> [Tue, 26 Oct 2021 11:15:40 +0100] rev 74590
Added / moved some simple set-theoretic lemmas
Tue, 26 Oct 2021 15:11:40 +0200 more CONTRIBUTORS and NEWS;
changeset
wenzelm [Tue, 26 Oct 2021 15:11:40 +0200] rev 74589
more CONTRIBUTORS and NEWS;
Tue, 19 Oct 2021 10:41:38 +0200 cleanup; add Apple reference
changeset
Norbert Schirmer <nschirmer@apple.com> [Tue, 19 Oct 2021 10:41:38 +0200] rev 74588
cleanup; add Apple reference
Thu, 15 Jul 2021 08:09:10 +0200 refine interface
changeset
Norbert Schirmer <nschirmer@apple.com> [Thu, 15 Jul 2021 08:09:10 +0200] rev 74587
refine interface
Thu, 12 Nov 2020 17:01:52 +0100 generalized component lookup for syntax and distinctness proofs. added some tracing.
changeset
Norbert Schirmer <nschirmer@apple.com> [Thu, 12 Nov 2020 17:01:52 +0100] rev 74586
generalized component lookup for syntax and distinctness proofs. added some tracing.
Mon, 25 Oct 2021 23:10:06 +0200 merged
changeset
wenzelm [Mon, 25 Oct 2021 23:10:06 +0200] rev 74585
merged
Mon, 25 Oct 2021 21:58:11 +0200 tuned;
changeset
wenzelm [Mon, 25 Oct 2021 21:58:11 +0200] rev 74584
tuned;
Mon, 25 Oct 2021 21:46:38 +0200 more antiquotations;
changeset
wenzelm [Mon, 25 Oct 2021 21:46:38 +0200] rev 74583
more antiquotations;
Mon, 25 Oct 2021 21:31:35 +0200 more antiquotations;
changeset
wenzelm [Mon, 25 Oct 2021 21:31:35 +0200] rev 74582
more antiquotations;
Mon, 25 Oct 2021 20:38:58 +0200 more robust: genuinely free variables need to be instantiated;
changeset
wenzelm [Mon, 25 Oct 2021 20:38:58 +0200] rev 74581
more robust: genuinely free variables need to be instantiated;
Mon, 25 Oct 2021 19:52:12 +0200 tuned comments;
changeset
wenzelm [Mon, 25 Oct 2021 19:52:12 +0200] rev 74580
tuned comments;
Mon, 25 Oct 2021 19:23:09 +0200 clarified errors;
changeset
wenzelm [Mon, 25 Oct 2021 19:23:09 +0200] rev 74579
clarified errors;
Mon, 25 Oct 2021 17:40:49 +0200 tuned;
changeset
wenzelm [Mon, 25 Oct 2021 17:40:49 +0200] rev 74578
tuned;
Mon, 25 Oct 2021 17:37:24 +0200 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
changeset
wenzelm [Mon, 25 Oct 2021 17:37:24 +0200] rev 74577
clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
Mon, 25 Oct 2021 17:26:27 +0200 tuned;
changeset
wenzelm [Mon, 25 Oct 2021 17:26:27 +0200] rev 74576
tuned;
Mon, 25 Oct 2021 11:41:03 +0200 clarified signature -- avoid clones;
changeset
wenzelm [Mon, 25 Oct 2021 11:41:03 +0200] rev 74575
clarified signature -- avoid clones;
Mon, 25 Oct 2021 13:56:08 +0100 Refinement of partitions
changeset
paulson <lp15@cam.ac.uk> [Mon, 25 Oct 2021 13:56:08 +0100] rev 74574
Refinement of partitions
Sun, 24 Oct 2021 22:10:28 +0200 avoid persistence of static context: instantiation arguments should provide proper dynamic context;
changeset
wenzelm [Sun, 24 Oct 2021 22:10:28 +0200] rev 74573
avoid persistence of static context: instantiation arguments should provide proper dynamic context;
Sun, 24 Oct 2021 21:59:36 +0200 more antiquotations;
changeset
wenzelm [Sun, 24 Oct 2021 21:59:36 +0200] rev 74572
more antiquotations;
Sun, 24 Oct 2021 21:19:55 +0200 more markup;
changeset
wenzelm [Sun, 24 Oct 2021 21:19:55 +0200] rev 74571
more markup;
Sun, 24 Oct 2021 20:25:51 +0200 clarified name, syntax, messages;
changeset
wenzelm [Sun, 24 Oct 2021 20:25:51 +0200] rev 74570
clarified name, syntax, messages;
Sun, 24 Oct 2021 18:29:21 +0200 more antiquotations;
changeset
wenzelm [Sun, 24 Oct 2021 18:29:21 +0200] rev 74569
more antiquotations;
Sun, 24 Oct 2021 18:02:58 +0200 more control symbols;
changeset
wenzelm [Sun, 24 Oct 2021 18:02:58 +0200] rev 74568
more control symbols;
Sun, 24 Oct 2021 16:43:54 +0200 tuned signature;
changeset
wenzelm [Sun, 24 Oct 2021 16:43:54 +0200] rev 74567
tuned signature;
Sun, 24 Oct 2021 16:38:13 +0200 ML antiquotations to instantiate types/terms/props;
changeset
wenzelm [Sun, 24 Oct 2021 16:38:13 +0200] rev 74566
ML antiquotations to instantiate types/terms/props;
Thu, 21 Oct 2021 18:20:08 +0200 tuned;
changeset
wenzelm [Thu, 21 Oct 2021 18:20:08 +0200] rev 74565
tuned;
Thu, 21 Oct 2021 18:10:51 +0200 clarified modules;
changeset
wenzelm [Thu, 21 Oct 2021 18:10:51 +0200] rev 74564
clarified modules;
Wed, 20 Oct 2021 20:25:33 +0200 clarified modules;
changeset
wenzelm [Wed, 20 Oct 2021 20:25:33 +0200] rev 74563
clarified modules;
Wed, 20 Oct 2021 20:04:28 +0200 clarified modules;
changeset
wenzelm [Wed, 20 Oct 2021 20:04:28 +0200] rev 74562
clarified modules;
Wed, 20 Oct 2021 18:13:17 +0200 discontinued obsolete "val extend = I" for data slots;
changeset
wenzelm [Wed, 20 Oct 2021 18:13:17 +0200] rev 74561
discontinued obsolete "val extend = I" for data slots;
Wed, 20 Oct 2021 17:11:46 +0200 clarified modules;
changeset
wenzelm [Wed, 20 Oct 2021 17:11:46 +0200] rev 74560
clarified modules;
Wed, 20 Oct 2021 16:45:10 +0200 clarified modules;
changeset
wenzelm [Wed, 20 Oct 2021 16:45:10 +0200] rev 74559
clarified modules;
Wed, 20 Oct 2021 16:36:49 +0200 clarified signature;
changeset
wenzelm [Wed, 20 Oct 2021 16:36:49 +0200] rev 74558
clarified signature;
Wed, 20 Oct 2021 11:34:28 +0200 tuned;
changeset
wenzelm [Wed, 20 Oct 2021 11:34:28 +0200] rev 74557
tuned;
Wed, 20 Oct 2021 11:25:32 +0200 clarified keywords and reports;
changeset
wenzelm [Wed, 20 Oct 2021 11:25:32 +0200] rev 74556
clarified keywords and reports;
Wed, 20 Oct 2021 10:47:34 +0200 clarified signature;
changeset
wenzelm [Wed, 20 Oct 2021 10:47:34 +0200] rev 74555
clarified signature;
Wed, 20 Oct 2021 09:31:37 +0200 merged
changeset
desharna [Wed, 20 Oct 2021 09:31:37 +0200] rev 74554
merged
Tue, 19 Oct 2021 11:48:31 +0200 proper veriT --max-time option
changeset
desharna [Tue, 19 Oct 2021 11:48:31 +0200] rev 74553
proper veriT --max-time option
Tue, 19 Oct 2021 11:29:02 +0200 refactored tptp_builtins in Sledgehammer
changeset
desharna [Tue, 19 Oct 2021 11:29:02 +0200] rev 74552
refactored tptp_builtins in Sledgehammer
Tue, 19 Oct 2021 18:24:33 +0200 merged
changeset
wenzelm [Tue, 19 Oct 2021 18:24:33 +0200] rev 74551
merged
Tue, 19 Oct 2021 17:30:01 +0200 tuned ML --- clarified use of context;
changeset
wenzelm [Tue, 19 Oct 2021 17:30:01 +0200] rev 74550
tuned ML --- clarified use of context; tuned message;
Tue, 19 Oct 2021 17:12:23 +0200 tuned --- fewer clones;
changeset
wenzelm [Tue, 19 Oct 2021 17:12:23 +0200] rev 74549
tuned --- fewer clones;
Tue, 19 Oct 2021 16:45:21 +0200 updated to jEdit plugin Highlight 2.5;
changeset
wenzelm [Tue, 19 Oct 2021 16:45:21 +0200] rev 74548
updated to jEdit plugin Highlight 2.5;
Tue, 19 Oct 2021 15:20:31 +0200 proper tactic combinator;
changeset
wenzelm [Tue, 19 Oct 2021 15:20:31 +0200] rev 74547
proper tactic combinator;
Tue, 19 Oct 2021 15:03:00 +0200 proper file headers;
changeset
wenzelm [Tue, 19 Oct 2021 15:03:00 +0200] rev 74546
proper file headers;
Tue, 19 Oct 2021 14:58:22 +0200 clarified context;
changeset
wenzelm [Tue, 19 Oct 2021 14:58:22 +0200] rev 74545
clarified context; clarified modules;
Tue, 19 Oct 2021 14:41:29 +0200 more accurate treatment of context;
changeset
wenzelm [Tue, 19 Oct 2021 14:41:29 +0200] rev 74544
more accurate treatment of context;
Tue, 19 Oct 2021 16:10:36 +0200 updated email address
changeset
Manuel Eberl <manuel@pruvisto.org> [Tue, 19 Oct 2021 16:10:36 +0200] rev 74543
updated email address
Fri, 15 Oct 2021 18:09:34 +0200 removed some 'private' modifiers from HOL-Computational_Algebra
changeset
Manuel Eberl <manuel@pruvisto.org> [Fri, 15 Oct 2021 18:09:34 +0200] rev 74542
removed some 'private' modifiers from HOL-Computational_Algebra
Mon, 18 Oct 2021 18:33:46 +0200 merged
changeset
wenzelm [Mon, 18 Oct 2021 18:33:46 +0200] rev 74541
merged
Mon, 18 Oct 2021 11:49:01 +0200 merged
changeset
wenzelm [Mon, 18 Oct 2021 11:49:01 +0200] rev 74540
merged
Mon, 18 Oct 2021 11:40:57 +0200 more robust Variable.revert_bounds (see also b12f2cef3ee5);
changeset
wenzelm [Mon, 18 Oct 2021 11:40:57 +0200] rev 74539
more robust Variable.revert_bounds (see also b12f2cef3ee5);
Sun, 17 Oct 2021 19:46:01 +0200 more accurate treatment of context;
changeset
wenzelm [Sun, 17 Oct 2021 19:46:01 +0200] rev 74538
more accurate treatment of context;
Sun, 17 Oct 2021 17:42:18 +0200 tuned -- proper names/scopes for contexts;
changeset
wenzelm [Sun, 17 Oct 2021 17:42:18 +0200] rev 74537
tuned -- proper names/scopes for contexts;
Sat, 16 Oct 2021 21:20:15 +0200 clarified context;
changeset
wenzelm [Sat, 16 Oct 2021 21:20:15 +0200] rev 74536
clarified context;
Sat, 16 Oct 2021 21:15:28 +0200 clarified context;
changeset
wenzelm [Sat, 16 Oct 2021 21:15:28 +0200] rev 74535
clarified context;
Sat, 16 Oct 2021 21:14:24 +0200 tuned;
changeset
wenzelm [Sat, 16 Oct 2021 21:14:24 +0200] rev 74534
tuned;
Sat, 16 Oct 2021 20:32:25 +0200 unused;
changeset
wenzelm [Sat, 16 Oct 2021 20:32:25 +0200] rev 74533
unused;
Sat, 16 Oct 2021 20:21:13 +0200 more accurate treatment of context;
changeset
wenzelm [Sat, 16 Oct 2021 20:21:13 +0200] rev 74532
more accurate treatment of context; declare generated bounds for the sake of recdef, which has variables leaking from local context;
Fri, 15 Oct 2021 22:49:07 +0200 isabelle regenerate_cooper;
changeset
wenzelm [Fri, 15 Oct 2021 22:49:07 +0200] rev 74531
isabelle regenerate_cooper;
Fri, 15 Oct 2021 22:00:28 +0200 revert bbfed17243af, breaks HOL-Proofs extraction;
changeset
wenzelm [Fri, 15 Oct 2021 22:00:28 +0200] rev 74530
revert bbfed17243af, breaks HOL-Proofs extraction;
Fri, 15 Oct 2021 21:59:46 +0200 tuned;
changeset
wenzelm [Fri, 15 Oct 2021 21:59:46 +0200] rev 74529
tuned;
Fri, 15 Oct 2021 21:25:47 +0200 tuned;
changeset
wenzelm [Fri, 15 Oct 2021 21:25:47 +0200] rev 74528
tuned;
Fri, 15 Oct 2021 21:10:54 +0200 proper p' instead of p (amending 52c7c42e7e27);
changeset
wenzelm [Fri, 15 Oct 2021 21:10:54 +0200] rev 74527
proper p' instead of p (amending 52c7c42e7e27);
Fri, 15 Oct 2021 20:54:13 +0200 proper context for Goal.prove_internal;
changeset
wenzelm [Fri, 15 Oct 2021 20:54:13 +0200] rev 74526
proper context for Goal.prove_internal;
Fri, 15 Oct 2021 19:25:31 +0200 discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
changeset
wenzelm [Fri, 15 Oct 2021 19:25:31 +0200] rev 74525
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily; Simplifier and equational conversions demand a proper proof context;
Fri, 15 Oct 2021 17:45:47 +0200 more accurate treatment of context, notably for nested Goal.proof / SUBPROOF;
changeset
wenzelm [Fri, 15 Oct 2021 17:45:47 +0200] rev 74524
more accurate treatment of context, notably for nested Goal.proof / SUBPROOF;
Fri, 15 Oct 2021 14:18:11 +0200 tuned;
changeset
wenzelm [Fri, 15 Oct 2021 14:18:11 +0200] rev 74523
tuned;
Fri, 15 Oct 2021 13:41:15 +0200 tuned;
changeset
wenzelm [Fri, 15 Oct 2021 13:41:15 +0200] rev 74522
tuned;
Fri, 15 Oct 2021 12:55:21 +0200 tuned;
changeset
wenzelm [Fri, 15 Oct 2021 12:55:21 +0200] rev 74521
tuned;
Fri, 15 Oct 2021 11:42:36 +0200 spelling;
changeset
wenzelm [Fri, 15 Oct 2021 11:42:36 +0200] rev 74520
spelling;
Fri, 15 Oct 2021 01:44:52 +0200 clarified context;
changeset
wenzelm [Fri, 15 Oct 2021 01:44:52 +0200] rev 74519
clarified context;
(0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 tip
isabelle