src/Pure/codegen.ML
Sun, 25 Oct 2009 20:54:21 +0100 wenzelm maintain theory name via name space, not tags;
Sat, 24 Oct 2009 19:20:03 +0200 wenzelm eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Mon, 19 Oct 2009 16:47:21 +0200 berghofe Removed dead code in function mk_deftab.
Sat, 17 Oct 2009 16:58:03 +0200 wenzelm operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Fri, 24 Jul 2009 22:59:28 +0200 wenzelm eliminated OldGoals.read_term;
Mon, 20 Jul 2009 16:11:00 +0200 haftmann deftab: only process theorems on demand
Tue, 14 Jul 2009 16:27:33 +0200 haftmann more accessors to unfold simpset
Thu, 14 May 2009 15:11:41 +0200 haftmann merged
Thu, 14 May 2009 15:09:46 +0200 haftmann quickcheck size starts with 0
Wed, 13 May 2009 19:21:32 +0200 berghofe Cleaned up code of function test_term.
Tue, 12 May 2009 19:30:33 +0200 haftmann transferred code generator preprocessor into separate module
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Thu, 05 Mar 2009 19:48:02 +0100 wenzelm Thm.add_oracle interface: replaced old bstring by binding;
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm use regular Term.add_vars, Term.add_frees etc.;
Mon, 15 Dec 2008 09:58:45 +0100 haftmann moved value.ML to src/Tools
Thu, 23 Oct 2008 15:28:01 +0200 wenzelm renamed Thm.get_axiom_i to Thm.axiom;
Sun, 19 Oct 2008 21:19:27 +0200 berghofe - removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML)
Thu, 09 Oct 2008 08:47:27 +0200 haftmann established canonical argument order in SML code generators
Fri, 26 Sep 2008 19:07:56 +0200 wenzelm eliminated polymorphic equality;
Mon, 22 Sep 2008 13:56:04 +0200 haftmann generic quickcheck framework
Mon, 22 Sep 2008 08:00:26 +0200 haftmann some steps towards generic quickcheck framework
Thu, 18 Sep 2008 19:39:50 +0200 wenzelm eval_term: CRITICAL due to eval_result;
Wed, 17 Sep 2008 21:27:34 +0200 wenzelm simplified ML_Context.eval_in -- expect immutable Proof.context value;
Tue, 16 Sep 2008 09:21:22 +0200 haftmann generic value command
Thu, 28 Aug 2008 22:09:20 +0200 haftmann restructured and split code serializer module
Wed, 06 Aug 2008 00:58:27 +0200 berghofe Reverted last change, since it caused incompatibilities.
Mon, 04 Aug 2008 18:57:35 +0200 berghofe Quoted terms in consts_code declarations are now preprocessed as well.
Mon, 30 Jun 2008 13:41:33 +0200 haftmann simplified retrieval of theory names of consts and types
Wed, 25 Jun 2008 17:38:32 +0200 wenzelm moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
Fri, 20 Jun 2008 21:00:26 +0200 haftmann type constructors now with markup
Wed, 18 Jun 2008 18:54:59 +0200 wenzelm OldGoals.simple_read_term;
Fri, 23 May 2008 16:37:57 +0200 berghofe Replaced Pretty.str and Pretty.string_of by specific functions that
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sat, 17 May 2008 15:31:42 +0200 wenzelm cat_lines;
Thu, 17 Apr 2008 16:30:45 +0200 wenzelm Pretty.mark;
Sat, 12 Apr 2008 17:00:35 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Fri, 28 Mar 2008 20:02:04 +0100 wenzelm Context.>> : operate on Context.generic;
Fri, 28 Mar 2008 00:02:54 +0100 wenzelm reorganized signature of ML_Context;
Thu, 27 Mar 2008 15:32:15 +0100 wenzelm eliminated delayed theory setup
Mon, 24 Mar 2008 23:34:24 +0100 wenzelm ML runtime compilation: pass position, tuned signature;
Thu, 10 Jan 2008 19:28:02 +0100 berghofe Test data generation and conversion to terms are now more closely
Sun, 11 Nov 2007 16:50:30 +0100 wenzelm auto quickcheck: reduced messages;
Sat, 10 Nov 2007 15:58:18 +0100 wenzelm auto_quickcheck ref: set default in ProofGeneral/preferences only
Fri, 09 Nov 2007 23:24:30 +0100 haftmann explicit message for failed autoquickcheck
Thu, 08 Nov 2007 22:57:45 +0100 wenzelm oops -- avoid vacous goal message;
Thu, 08 Nov 2007 22:36:46 +0100 wenzelm tuned messages;
Tue, 06 Nov 2007 13:12:50 +0100 haftmann autoquickcheck message
Fri, 12 Oct 2007 18:09:12 +0200 wenzelm eval_term: moved actual evaluation out of CRITICAL section;
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Mon, 08 Oct 2007 18:13:07 +0200 wenzelm Codegen.is_instance: raw match, ignore sort constraints;
Sat, 06 Oct 2007 16:50:04 +0200 wenzelm simplified interfaces for outer syntax;
Mon, 01 Oct 2007 21:19:53 +0200 wenzelm auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
Tue, 25 Sep 2007 13:28:37 +0200 wenzelm Syntax.parse/check/read;
less more (0) -100 -60 tip