Sat, 14 Apr 2012 23:34:18 +0200 |
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
|
file | diff | annotate |
Thu, 12 Apr 2012 18:39:19 +0200 |
more standard method setup;
|
file | diff | annotate |
Tue, 27 Mar 2012 14:49:56 +0200 |
remove redundant lemmas
|
file | diff | annotate |
Sun, 25 Mar 2012 20:15:39 +0200 |
merged fork with new numeral representation (see NEWS)
|
file | diff | annotate |
Wed, 15 Feb 2012 23:19:30 +0100 |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file | diff | annotate |
Fri, 02 Dec 2011 14:54:25 +0100 |
more antiquotations;
|
file | diff | annotate |
Wed, 23 Nov 2011 22:59:39 +0100 |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file | diff | annotate |
Wed, 19 Oct 2011 15:42:43 +0200 |
inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
|
file | diff | annotate |
Wed, 10 Aug 2011 20:53:43 +0200 |
old term operations are legacy;
|
file | diff | annotate |
Wed, 29 Jun 2011 17:35:46 +0200 |
modernized some simproc setup;
|
file | diff | annotate |
Thu, 09 Jun 2011 23:12:02 +0200 |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file | diff | annotate |
Fri, 13 May 2011 22:55:00 +0200 |
proper Proof.context for classical tactics;
|
file | diff | annotate |
Sat, 16 Apr 2011 16:15:37 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
Fri, 08 Apr 2011 13:31:16 +0200 |
explicit structure Syntax_Trans;
|
file | diff | annotate |
Sat, 08 Jan 2011 17:14:48 +0100 |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file | diff | annotate |
Mon, 06 Sep 2010 19:13:10 +0200 |
more antiquotations;
|
file | diff | annotate |
Sat, 28 Aug 2010 16:14:32 +0200 |
formerly unnamed infix equality now named HOL.eq
|
file | diff | annotate |
Fri, 27 Aug 2010 17:59:40 +0200 |
more antiquotations;
|
file | diff | annotate |
Fri, 27 Aug 2010 10:56:46 +0200 |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file | diff | annotate |
Thu, 26 Aug 2010 20:51:17 +0200 |
formerly unnamed infix impliciation now named HOL.implies
|
file | diff | annotate |
Thu, 19 Aug 2010 16:08:59 +0200 |
tuned quotes
|
file | diff | annotate |
Thu, 19 Aug 2010 11:02:14 +0200 |
use antiquotations for remaining unqualified constants in HOL
|
file | diff | annotate |
Tue, 08 Jun 2010 16:37:22 +0200 |
tuned quotes, antiquotations and whitespace
|
file | diff | annotate |
Tue, 25 May 2010 20:28:16 +0200 |
eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
|
file | diff | annotate |
Sat, 15 May 2010 21:50:05 +0200 |
less pervasive names from structure Thm;
|
file | diff | annotate |
Tue, 11 May 2010 19:00:16 +0200 |
represent de-Bruin indices simply by position in list
|
file | diff | annotate |
Tue, 11 May 2010 18:46:03 +0200 |
tuned reification functions
|
file | diff | annotate |
Tue, 11 May 2010 18:31:36 +0200 |
tuned code; toward a tightended interface with generated code
|
file | diff | annotate |
Mon, 10 May 2010 15:33:32 +0200 |
tuned; dropped strange myassoc2
|
file | diff | annotate |
Mon, 10 May 2010 15:24:43 +0200 |
stylized COOPER exception
|
file | diff | annotate |
Mon, 10 May 2010 15:21:13 +0200 |
simplified oracle
|
file | diff | annotate |
Mon, 10 May 2010 15:00:53 +0200 |
shorten names
|
file | diff | annotate |
Mon, 10 May 2010 14:55:06 +0200 |
only one module fpr presburger method
|
file | diff | annotate |
Mon, 10 May 2010 14:11:50 +0200 |
one structure is better than three
|
file | diff | annotate |
Mon, 10 May 2010 13:58:18 +0200 |
less complex organization of cooper source code
|
file | diff | annotate |
Mon, 10 May 2010 12:25:49 +0200 |
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
|
file | diff | annotate |
Thu, 06 May 2010 19:27:51 +0200 |
merged
|
file | diff | annotate |
Thu, 06 May 2010 16:32:21 +0200 |
tuned whitespace; dropped superfluous open
|
file | diff | annotate |
Wed, 05 May 2010 18:25:34 +0200 |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file | diff | annotate |
Wed, 28 Apr 2010 21:41:05 +0200 |
modernized structure name
|
file | diff | annotate |
Sun, 28 Feb 2010 23:51:31 +0100 |
more antiquotations;
|
file | diff | annotate |
Fri, 19 Feb 2010 14:47:01 +0100 |
moved remaning class operations from Algebras.thy to Groups.thy
|
file | diff | annotate |
Wed, 10 Feb 2010 14:12:04 +0100 |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
file | diff | annotate |
Mon, 08 Feb 2010 17:12:38 +0100 |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file | diff | annotate |
Thu, 28 Jan 2010 11:48:49 +0100 |
new theory Algebras.thy for generic algebraic structures
|
file | diff | annotate |
Wed, 21 Oct 2009 12:02:56 +0200 |
curried union as canonical list operation
|
file | diff | annotate |
Wed, 21 Oct 2009 08:16:25 +0200 |
merged
|
file | diff | annotate |
Wed, 21 Oct 2009 08:14:38 +0200 |
dropped redundant gen_ prefix
|
file | diff | annotate |
Tue, 20 Oct 2009 16:13:01 +0200 |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file | diff | annotate |
Wed, 21 Oct 2009 00:36:12 +0200 |
standardized basic operations on type option;
|
file | diff | annotate |
Mon, 19 Oct 2009 21:54:57 +0200 |
uniform use of Integer.add/mult/sum/prod;
|
file | diff | annotate |
Fri, 18 Sep 2009 09:07:50 +0200 |
tuned const_name antiquotations
|
file | diff | annotate |
Fri, 28 Aug 2009 18:18:30 +0200 |
modernized messages -- eliminated old Display.print_cterm;
|
file | diff | annotate |
Mon, 24 Aug 2009 10:44:03 +0200 |
stricter condition for (binary) integer relation
|
file | diff | annotate |
Tue, 28 Jul 2009 13:37:09 +0200 |
Set.UNIV and Set.empty are mere abbreviations for top and bot
|
file | diff | annotate |
Mon, 11 May 2009 15:57:29 +0200 |
qualified names for Lin_Arith tactics and simprocs
|
file | diff | annotate |
Mon, 23 Mar 2009 19:01:16 +0100 |
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
|
file | diff | annotate |
Thu, 19 Mar 2009 22:05:00 +0100 |
proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
|
file | diff | annotate |
Wed, 11 Mar 2009 15:56:50 +0100 |
tuned funny error message
|
file | diff | annotate |
Thu, 05 Mar 2009 08:23:11 +0100 |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file | diff | annotate |