src/HOL/Library/Old_Datatype.thy
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Tue, 02 Jan 2018 16:17:13 +0100 blanchet moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
Tue, 02 Jan 2018 16:11:20 +0100 blanchet removed 'old_datatype' command
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Wed, 19 Apr 2017 16:26:09 +0200 wenzelm tuned imports;
Mon, 11 Jan 2016 21:21:02 +0100 wenzelm eliminated old defs;
Mon, 28 Dec 2015 17:43:30 +0100 wenzelm prefer symbols for "Union", "Inter";
Sun, 27 Dec 2015 22:07:17 +0100 wenzelm discontinued ASCII replacement syntax <*>;
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Fri, 19 Sep 2014 13:27:04 +0200 blanchet keep obsolete interpretations in Main, to avoid merge trouble
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved old 'size' generator together with 'old_datatype'
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved datatype realizer to 'old_datatype' and colleagues
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
less more (0) tip