src/Pure/raw_simplifier.ML
Sun, 09 Jun 2024 15:31:33 +0200 wenzelm more accurate thm "name_hint", using Thm_Name.T;
Sun, 09 Jun 2024 12:29:04 +0200 wenzelm tuned;
Mon, 01 Apr 2024 15:47:15 +0200 wenzelm clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code;
Mon, 01 Apr 2024 15:37:55 +0200 wenzelm clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);
Tue, 27 Feb 2024 17:06:19 +0100 nipkow tuned name
Tue, 27 Feb 2024 11:59:47 +0100 nipkow new simplifier trace_op for tracing simproc calls
Tue, 27 Feb 2024 10:49:48 +0100 nipkow simplifier: no trace info from simprocs unless simp_debug = true.
Sun, 22 Oct 2023 13:56:52 +0200 wenzelm tuned;
Sat, 21 Oct 2023 21:19:02 +0200 wenzelm simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
Thu, 19 Oct 2023 17:06:39 +0200 wenzelm clarified signature;
Tue, 25 Jul 2023 14:12:26 +0200 wenzelm performance tuning: prefer static simpset within functional closure of morphism (with notable impact on specifications "in" class, e.g. AFP/No_FTL_observers);
Tue, 06 Jun 2023 11:33:38 +0200 wenzelm tuned;
Fri, 26 May 2023 13:19:49 +0200 wenzelm clarified treatment of context;
Sat, 20 May 2023 16:12:37 +0200 wenzelm more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
Fri, 19 May 2023 21:22:39 +0200 wenzelm clarified signature;
Fri, 19 May 2023 11:41:30 +0200 wenzelm more careful reset_context for stored entity;
Thu, 18 May 2023 17:21:29 +0200 wenzelm clarified signature: more explicit types;
Mon, 15 May 2023 14:09:45 +0200 wenzelm more operations "without_context", assuming that the thm has been properly transferred already;
Mon, 15 May 2023 10:59:49 +0200 wenzelm tuned: more accurate check (is_norm_hhf protect);
Tue, 18 Apr 2023 22:24:48 +0200 wenzelm tuned;
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();
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;
Wed, 13 Oct 2021 13:19:09 +0200 wenzelm clarified signature;
Fri, 10 Sep 2021 14:59:19 +0200 wenzelm clarified signature: more scalable operations;
Thu, 09 Sep 2021 12:33:14 +0200 wenzelm clarified signature;
Sat, 04 Sep 2021 21:25:08 +0200 wenzelm clarified signature;
Sat, 04 Sep 2021 13:49:26 +0200 wenzelm more scalable operations;
less more (0) -100 -50 -30 tip