src/Pure/Isar/code.ML
Sat, 18 Feb 2012 11:31:35 +0100 haftmann more explicit error on malformed abstract equation; dropped dead code; tuned signature
Mon, 26 Dec 2011 18:32:43 +0100 haftmann dropped disfruitful `constant signatures`
Wed, 09 Nov 2011 21:36:18 +0100 wenzelm misc tuning;
Sat, 05 Nov 2011 15:00:49 +0100 wenzelm added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
Wed, 19 Oct 2011 23:07:48 +0200 haftmann removed some remaining artefacts of ancient SML code generator
Wed, 06 Jul 2011 20:46:06 +0200 wenzelm prefer Synchronized.var;
Sat, 02 Jul 2011 10:37:35 +0200 haftmann correction: do not assume that case const index covered all cases
Fri, 01 Jul 2011 23:31:23 +0200 haftmann remove illegal case combinators after merge
Fri, 01 Jul 2011 23:10:27 +0200 haftmann corrected misunderstanding what `old functions` are supposed to be
Fri, 01 Jul 2011 23:07:06 +0200 haftmann centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be
Fri, 01 Jul 2011 19:57:41 +0200 haftmann index cases for constructors
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Fri, 06 May 2011 11:57:21 +0200 bulwahn improving merge of code specifications by removing code equations of constructors after merging two theories
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 15:25:25 +0200 wenzelm prefer local name spaces;
Mon, 10 Jan 2011 16:45:28 +0100 wenzelm added merge_options convenience;
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Wed, 01 Dec 2010 15:03:44 +0100 wenzelm more direct use of binder_types/body_type;
Mon, 29 Nov 2010 11:38:59 +0100 haftmann tuned
Sat, 27 Nov 2010 22:01:27 +0100 haftmann typscheme with signatures is inappropriate when building empty certificate;
Sat, 27 Nov 2010 19:41:28 +0100 haftmann corrected: use canonical variables of type scheme uniformly
Fri, 26 Nov 2010 23:49:49 +0100 haftmann consider sort constraints for datatype constructors when constructing the empty equation certificate;
Fri, 26 Nov 2010 22:33:21 +0100 haftmann keep type variable arguments of datatype constructors in bookkeeping
Tue, 16 Nov 2010 10:33:36 +0100 haftmann added forall2 predicate lifter
Thu, 04 Nov 2010 17:27:38 +0100 haftmann Code.check_const etc.: reject too specific types
Wed, 03 Nov 2010 11:06:22 +0100 wenzelm replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
Tue, 26 Oct 2010 15:00:42 +0200 haftmann more general treatment of type argument in code certificates for operations on abstract types
Fri, 01 Oct 2010 10:25:36 +0200 haftmann chop_while replace drop_while and take_while
Thu, 30 Sep 2010 18:37:29 +0200 haftmann take_while, drop_while
Thu, 30 Sep 2010 08:50:45 +0200 haftmann corrected subsumption check: arguments have been reversed; addition of default equations to non-default equations is identity
Wed, 29 Sep 2010 15:28:29 +0200 haftmann redundancy check: drop trailing Var arguments (avoids eta problems with equations)
Mon, 20 Sep 2010 18:43:26 +0200 haftmann corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself
Mon, 20 Sep 2010 11:55:21 +0200 haftmann more accurate exception handling
Wed, 15 Sep 2010 15:11:39 +0200 haftmann ignore code cache optionally
Sun, 05 Sep 2010 21:41:24 +0200 wenzelm turned show_sorts/show_types into proper configuration options;
Wed, 01 Sep 2010 15:33:59 +0200 haftmann replaced Table.map' by Table.map
Mon, 23 Aug 2010 11:09:48 +0200 haftmann dropped now obsolete purge_data -- happens implicitly on change of theory identity
Thu, 24 Jun 2010 09:04:50 +0200 haftmann made smlnj happy
Fri, 18 Jun 2010 15:03:21 +0200 haftmann drop subsumed default equations (requires a little bit unfortunate laziness)
Thu, 17 Jun 2010 15:59:46 +0200 haftmann explicit type variable arguments for constructors
Tue, 15 Jun 2010 11:38:39 +0200 haftmann maintain cong rules for case combinators
Mon, 14 Jun 2010 12:01:30 +0200 haftmann explicitly name and note equations for class eq
Mon, 03 May 2010 20:13:36 +0200 wenzelm renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Mon, 19 Apr 2010 15:31:56 +0200 haftmann more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
Mon, 19 Apr 2010 11:30:08 +0200 haftmann explicit check sorts in abstract certificates; abstractor is part of dependencies
Tue, 13 Apr 2010 11:30:12 +0200 haftmann more accurate pattern match
Sun, 11 Apr 2010 16:51:07 +0200 haftmann user interface for abstract datatypes is an attribute, not a command
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Fri, 26 Feb 2010 10:48:21 +0100 haftmann use abstract code cerficates for bare code theorems
Wed, 24 Feb 2010 14:42:28 +0100 haftmann bound argument for abstype proposition
Wed, 24 Feb 2010 14:19:54 +0100 haftmann more precise exception handler
Mon, 22 Feb 2010 15:53:19 +0100 haftmann more accurate when registering new types
Mon, 22 Feb 2010 11:10:20 +0100 haftmann proper distinction of code datatypes and abstypes
Fri, 19 Feb 2010 11:06:21 +0100 haftmann a simple concept for datatype invariants
Thu, 14 Jan 2010 17:47:39 +0100 haftmann printing of cases
Wed, 13 Jan 2010 12:20:37 +0100 haftmann explicit abstract type of code certificates
less more (0) -100 -60 tip