src/HOL/Tools/rewrite_hol_proof.ML
Tue, 21 Apr 2020 22:19:59 +0200 wenzelm clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;
Fri, 08 Nov 2019 20:59:34 +0100 wenzelm tuned comments;
Sat, 12 Oct 2019 16:46:33 +0200 wenzelm early setup of proof preprocessing;
Fri, 11 Oct 2019 22:01:45 +0200 wenzelm proper ML names;
Fri, 09 Aug 2019 15:58:26 +0200 wenzelm clarified ML types;
Fri, 26 Jul 2019 14:43:56 +0200 wenzelm tuned signature;
Fri, 26 Jul 2019 09:35:02 +0200 wenzelm defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement;
Sun, 21 Jul 2019 15:19:07 +0200 wenzelm global declaration of abstract syntax for proof terms, with qualified names;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Mon, 27 Nov 2017 10:36:43 +0100 wenzelm more symbols;
Mon, 27 Nov 2017 10:21:52 +0100 wenzelm prefer Input.source (via cartouche);
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Thu, 03 Jun 2010 23:56:05 +0200 wenzelm do not open Proofterm, which is very ould style;
less more (0) -15 tip