src/HOL/UNITY/Comp/Alloc.thy
Tue, 16 Jan 2018 09:58:17 +0100 wenzelm tuned document;
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Wed, 25 May 2016 11:50:58 +0200 wenzelm isabelle update_cartouches -c -t;
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Mon, 28 Dec 2015 19:23:15 +0100 wenzelm more symbols;
Wed, 16 Dec 2015 16:31:36 +0100 wenzelm rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
Thu, 23 Jul 2015 22:13:42 +0200 wenzelm more symbols by default, without xsymbols mode;
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Wed, 25 Mar 2015 10:44:57 +0100 wenzelm prefer local fixes;
Mon, 10 Nov 2014 21:49:48 +0100 wenzelm proper context for assume_tac (atac remains as fall-back without context);
Tue, 18 Mar 2014 11:07:47 +0100 wenzelm tuned signature -- rearranged modules;
Mon, 20 May 2013 18:38:28 +0200 wenzelm proper context;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Fri, 12 Apr 2013 17:21:51 +0200 wenzelm modifiers for classical wrappers operate on Proof.context instead of claset;
Tue, 13 Mar 2012 22:49:02 +0100 wenzelm tuned proofs;
Tue, 21 Feb 2012 17:09:17 +0100 wenzelm tuned proofs;
Sun, 20 Nov 2011 21:05:23 +0100 wenzelm eliminated obsolete "standard";
Sun, 20 Nov 2011 17:44:41 +0100 wenzelm 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
Sat, 10 Sep 2011 22:11:55 +0200 wenzelm misc tuning and clarification;
Sun, 15 May 2011 17:45:53 +0200 wenzelm simplified/unified method_setup/attribute_setup;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Thu, 12 May 2011 18:18:06 +0200 wenzelm prefer Proof.context over old-style clasimpset;
Mon, 22 Nov 2010 10:34:33 +0100 hoelzl Replace surj by abbreviation; remove surj_on.
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Mon, 06 Sep 2010 19:13:10 +0200 wenzelm more antiquotations;
Tue, 27 Jul 2010 17:09:35 +0200 haftmann delete structure Basic_Record; avoid `record` in names in structure Record
Thu, 22 Jul 2010 18:08:39 +0200 wenzelm updated some headers;
Wed, 12 May 2010 16:44:49 +0200 wenzelm modernized specifications;
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Wed, 22 Jul 2009 18:02:10 +0200 haftmann moved complete_lattice &c. into separate theory
Mon, 16 Mar 2009 18:24:30 +0100 wenzelm simplified method setup;
Sun, 15 Mar 2009 15:59:44 +0100 wenzelm simplified attribute setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Sun, 27 Jan 2008 22:21:39 +0100 wenzelm rename_client_map_tac: avoid ill-defined thm reference;
Fri, 03 Aug 2007 20:19:41 +0200 wenzelm misc cleanup of ML bindings (for multihreading);
Fri, 08 Dec 2006 18:22:28 +0100 paulson patched up the proofs agsin
Wed, 06 Dec 2006 01:12:36 +0100 wenzelm removed legacy ML bindings;
Mon, 04 Dec 2006 00:05:47 +0100 wenzelm converted legacy ML script;
Wed, 07 Sep 2005 21:00:30 +0200 wenzelm converted to Isar theory format;
Thu, 22 Jul 2004 17:37:31 +0200 nipkow Modified \<Sum> syntax a little.
Mon, 15 Oct 2001 20:42:06 +0200 wenzelm setsum syntax;
Mon, 05 Mar 2001 15:32:54 +0100 paulson reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
less more (0) tip