src/HOL/Boogie/Tools/boogie_loader.ML
Tue, 27 Mar 2012 17:11:02 +0200 boehmes dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Sat, 23 Jul 2011 16:37:17 +0200 wenzelm defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
Fri, 08 Jul 2011 14:37:19 +0200 wenzelm more abstract Thy_Load.load_file/use_file for external theory resources;
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;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 08 Apr 2011 15:02:11 +0200 wenzelm discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
Wed, 24 Nov 2010 10:39:58 +0100 boehmes be more precise: only treat constant 'distinct' applied to an explicit list as built-in
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
Fri, 29 Oct 2010 18:17:04 +0200 boehmes introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
Thu, 26 Aug 2010 20:51:17 +0200 haftmann formerly unnamed infix impliciation now named HOL.implies
Sun, 08 Aug 2010 04:28:51 +0200 boehmes added scanning of if-then-else expressions
Wed, 26 May 2010 15:34:47 +0200 boehmes hide constants and types introduced by SMT,
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
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, 22 Mar 2010 19:25:14 +0100 wenzelm use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);
Mon, 22 Mar 2010 09:40:11 +0100 boehmes replaced old-style Drule.add_axiom by Specification.axiomatization
Mon, 22 Mar 2010 00:48:56 +0100 wenzelm replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
Thu, 18 Mar 2010 23:08:52 +0100 wenzelm typedecl: no sort constraints;
Tue, 09 Mar 2010 23:32:49 +0100 wenzelm Typedecl.typedecl_global;
Sun, 07 Mar 2010 12:47:02 +0100 wenzelm separate structure Typedecl;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Fri, 26 Feb 2010 23:07:27 +0100 wenzelm tuned;
Fri, 26 Feb 2010 23:05:47 +0100 wenzelm use simplified Syntax.escape;
Thu, 25 Feb 2010 09:16:16 +0100 boehmes use mixfix syntax for Boogie types
Sun, 14 Feb 2010 17:46:28 +0100 boehmes optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
Fri, 22 Jan 2010 16:33:44 +0100 boehmes drop underscores at end of names coming from Boogie
Wed, 23 Dec 2009 17:35:56 +0100 boehmes merged verification condition structure and term representation in one datatype,
Fri, 11 Dec 2009 15:35:29 +0100 boehmes make assertion labels unique already when loading a verification condition,
Mon, 07 Dec 2009 09:12:16 +0100 boehmes verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
Wed, 25 Nov 2009 12:28:29 +0100 boehmes respect "unique" attribute: generate distinctness axioms
Fri, 13 Nov 2009 15:06:19 +0100 boehmes corrected translation of integer operators,
Fri, 06 Nov 2009 21:53:20 +0100 boehmes made SML/NJ happy
Fri, 06 Nov 2009 09:27:20 +0100 boehmes tuned
Thu, 05 Nov 2009 14:48:40 +0100 boehmes shorter names for variables and verification conditions,
Tue, 03 Nov 2009 23:44:16 +0100 boehmes proper and unique case names for the split_vc method,
Tue, 03 Nov 2009 17:54:24 +0100 boehmes added HOL-Boogie
less more (0) tip