src/HOL/Import/import_rule.ML
Mon, 03 Jun 2019 11:27:23 +0200 wenzelm redundant: default is false;
Thu, 21 Feb 2019 09:15:07 +0000 haftmann streamlined specification interfaces
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 26 Feb 2016 22:38:44 +0100 wenzelm take qualification of type name more seriously: derived consts and facts are qualified uniformly;
Sat, 27 Feb 2016 17:01:21 +0100 wenzelm no tracing SPAM, and thus more visible warnings;
Thu, 24 Sep 2015 13:33:42 +0200 wenzelm explicit indication of overloaded typedefs;
Thu, 03 Sep 2015 21:50:39 +0200 wenzelm more general Typedef.bindings;
Mon, 27 Jul 2015 17:44:55 +0200 wenzelm tuned signature;
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Sun, 05 Jul 2015 22:07:09 +0200 wenzelm clarified context;
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Wed, 03 Jun 2015 19:25:05 +0200 wenzelm clarified context;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Sun, 09 Nov 2014 20:49:28 +0100 wenzelm proper context for typedef;
Mon, 08 Sep 2014 23:04:18 +0200 blanchet added flag to 'typedef' to allow concealed definitions
Mon, 24 Mar 2014 16:19:24 +0100 wenzelm proper Sign.full_name to get internal name (like Sign.add_consts);
Sat, 22 Mar 2014 20:42:16 +0100 wenzelm more antiquotations;
Fri, 21 Mar 2014 10:45:03 +0100 wenzelm tuned signature;
Mon, 26 Nov 2012 14:43:28 +0100 wenzelm tuned command descriptions;
Fri, 12 Oct 2012 21:22:35 +0200 wenzelm discontinued typedef with alternative name;
Fri, 12 Oct 2012 15:08:29 +0200 wenzelm discontinued typedef with implicit set_def;
Wed, 22 Aug 2012 12:47:49 +0200 wenzelm clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
Thu, 05 Apr 2012 08:43:31 +0200 krauss added timestamps to logging of named thms
Wed, 04 Apr 2012 20:09:56 +0200 Cezary Kaliszyk HOL/Import typed matches against Isabelle typedef result
Sun, 01 Apr 2012 14:50:47 +0200 Cezary Kaliszyk Modernized HOL-Import for HOL Light
less more (0) tip