src/HOL/Tools/Quickcheck/random_generators.ML
Sat, 13 Apr 2019 22:06:40 +0200 wenzelm tuned signature;
Sat, 13 Apr 2019 16:26:19 +0200 wenzelm tuned signature -- more ctyp operations;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 06 Dec 2017 20:43:09 +0100 wenzelm prefer control symbol antiquotations;
Sun, 02 Jul 2017 20:13:38 +0200 haftmann proper concept of code declaration wrt. atomicity and Isar declarations
Thu, 23 Jun 2016 11:01:14 +0200 wenzelm tuned signature;
Mon, 06 Jun 2016 21:28:46 +0200 haftmann explicit tagging of code equations de-baroquifies interface
Sun, 29 May 2016 15:40:25 +0200 wenzelm clarified check_open_spec / read_open_spec;
Thu, 28 Apr 2016 09:43:11 +0200 wenzelm support 'assumes' in specifications, e.g. 'definition', 'inductive';
Thu, 14 Apr 2016 15:33:51 +0200 wenzelm misc tuning and standardization;
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Sun, 06 Sep 2015 22:14:51 +0200 haftmann prefer "uncurry" as canonical name for case distinction on products in combinatorial view
Sat, 18 Jul 2015 20:47:08 +0200 wenzelm prefer tactics with explicit 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);
Fri, 10 Apr 2015 18:23:01 +0200 blanchet renamed ML funs
Tue, 31 Mar 2015 00:11:54 +0200 wenzelm tuned signature;
Fri, 06 Mar 2015 23:53:52 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Fri, 06 Mar 2015 00:00:57 +0100 wenzelm tuned -- more explicit use of context;
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Fri, 19 Dec 2014 20:10:59 +0100 wenzelm just one data slot per program unit;
Fri, 19 Dec 2014 12:56:06 +0100 wenzelm proper exception for internal program failure, not user-error;
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
Mon, 13 Oct 2014 18:45:48 +0200 wenzelm Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
Mon, 08 Sep 2014 15:54:33 +0200 blanchet export right sorts
Mon, 08 Sep 2014 14:03:57 +0200 blanchet use compatibility layer
Fri, 05 Sep 2014 00:41:01 +0200 blanchet pretend code generation is a ctr_sugar plugin
Fri, 05 Sep 2014 00:41:01 +0200 blanchet named interpretations
Mon, 01 Sep 2014 16:17:46 +0200 blanchet renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
less more (0) -50 -30 tip