src/Pure/more_thm.ML
Sun, 11 Aug 2024 11:32:20 +0200 wenzelm tuned modules;
Sun, 09 Jun 2024 20:19:53 +0200 wenzelm clarified operations, including exceptions;
Sun, 09 Jun 2024 15:31:33 +0200 wenzelm more accurate thm "name_hint", using Thm_Name.T;
Mon, 08 Jan 2024 21:53:16 +0100 wenzelm minor performance tuning;
Tue, 25 Jul 2023 15:52:32 +0200 wenzelm tuned;
Tue, 06 Jun 2023 11:33:38 +0200 wenzelm tuned;
Tue, 18 Apr 2023 12:23:37 +0200 wenzelm backout 4a174bea55e2;
Mon, 17 Apr 2023 23:32:46 +0200 wenzelm revert b43ee37926a9 due to problems with AFP/PAPP_Impossibility;
Mon, 10 Apr 2023 22:38:18 +0200 wenzelm performance tuning: replace Ord_List by Set();
Tue, 28 Mar 2023 17:59:54 +0200 wenzelm prefer Sortset.T for shyps;
Mon, 27 Mar 2023 21:48:47 +0200 wenzelm performance tuning: prefer functor Set() over Table();
Thu, 08 Sep 2022 12:52:41 +0200 wenzelm tuned signature;
Sun, 24 Oct 2021 16:38:13 +0200 wenzelm ML antiquotations to instantiate types/terms/props;
Wed, 20 Oct 2021 18:13:17 +0200 wenzelm discontinued obsolete "val extend = I" for data slots;
Fri, 15 Oct 2021 19:25:31 +0200 wenzelm 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;
Thu, 14 Oct 2021 16:03:20 +0200 wenzelm clarified signature;
Fri, 10 Sep 2021 14:59:19 +0200 wenzelm clarified signature: more scalable operations;
Thu, 09 Sep 2021 15:55:12 +0200 wenzelm clarified signature;
Thu, 09 Sep 2021 15:45:27 +0200 wenzelm clarified modules;
Thu, 09 Sep 2021 14:50:26 +0200 wenzelm clarified set of items with order of addition;
Thu, 09 Sep 2021 12:33:14 +0200 wenzelm clarified signature;
Thu, 09 Sep 2021 10:40:57 +0200 wenzelm tuned;
Mon, 06 Sep 2021 14:05:22 +0200 wenzelm clarified modules;
Mon, 06 Sep 2021 12:46:08 +0200 wenzelm more scalable operations;
Mon, 06 Sep 2021 12:25:19 +0200 wenzelm tuned;
Mon, 06 Sep 2021 12:23:06 +0200 wenzelm clarified modules;
Mon, 06 Sep 2021 12:11:17 +0200 wenzelm clarified signature;
Mon, 06 Sep 2021 11:55:54 +0200 wenzelm more scalable operations;
Mon, 06 Sep 2021 11:39:44 +0200 wenzelm unused;
Mon, 06 Sep 2021 11:32:18 +0200 wenzelm more efficient operations: traverse hyps only when required;
less more (0) -100 -50 -30 tip