src/HOL/Quotient_Examples/Lift_FSet.thy
Fri, 18 Oct 2024 14:20:09 +0200 wenzelm more inner-syntax markup;
Tue, 01 Oct 2024 20:39:16 +0200 wenzelm drop somewhat pointless 'syntax_consts' declarations;
Mon, 30 Sep 2024 23:32:26 +0200 wenzelm clarified syntax: use outer block (with indent);
Mon, 30 Sep 2024 20:30:59 +0200 wenzelm clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
Fri, 20 Sep 2024 19:51:08 +0200 wenzelm standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
Wed, 28 Aug 2024 22:54:45 +0200 wenzelm more specific "args" syntax, to support more markup for syntax consts;
Sun, 25 Aug 2024 21:10:01 +0200 wenzelm more markup for syntax consts;
Thu, 28 Mar 2019 21:24:55 +0100 wenzelm "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Wed, 22 Jun 2016 10:09:20 +0200 wenzelm bundle lifting_syntax;
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Mon, 10 Nov 2014 10:29:19 +0100 traytel dropped redundant transfer rules (now proved and registered by datatype and plugins)
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 07 Aug 2014 12:17:41 +0200 blanchet no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
Tue, 25 Feb 2014 15:02:20 +0100 kuncar simplify and repair proofs due to df0fda378813
less more (0) -15 tip