| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned structure inclusion
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 14:29:22 +0100 |
wenzelm |
clarified simplifier context;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Sun, 30 Jun 2013 11:37:34 +0200 |
wenzelm |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 23:17:26 +0200 |
wenzelm |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 21:16:15 +0100 |
wenzelm |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 20:05:58 +0100 |
wenzelm |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 17:45:04 +0100 |
wenzelm |
discontinued old-style Term.list_all_free in favour of plain Logic.all;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2011 10:38:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 23:05:21 +0100 |
wenzelm |
datatype dtyp with explicit sort information;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 21:14:01 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 20:21:49 +0200 |
wenzelm |
added Reconstruct.proof_of convenience;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 18:11:20 +0200 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
| Thu, 03 Feb 2011 19:21:12 +0100 |
wenzelm |
clarified Proofterm.proofs_enabled;
|
file |
diff |
annotate
|
| Thu, 30 Dec 2010 23:42:06 +0100 |
wenzelm |
do not open auxiliary ML structures;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 15:03:44 +0100 |
wenzelm |
more direct use of binder_types/body_type;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 22:59:11 +0200 |
wenzelm |
eliminated really ancient OldGoals operations in favour of Goal.prove_internal (with its minimal checks and without normalization of result);
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 11:30:57 +0200 |
berghofe |
merged
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 11:13:09 +0200 |
berghofe |
Adapted to new format of proof terms containing explicit proofs of class membership.
|
file |
diff |
annotate
|
| Wed, 26 May 2010 16:05:25 +0200 |
haftmann |
dropped legacy theorem bindings
|
file |
diff |
annotate
|
| Sat, 08 May 2010 16:53:53 +0200 |
wenzelm |
renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
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
|
| 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;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:32:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 12:28:12 +0100 |
haftmann |
dropped some unused bindings
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 11:42:49 +0100 |
haftmann |
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 23:49:55 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 00:36:12 +0200 |
wenzelm |
standardized basic operations on type option;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 10:20:21 +0200 |
haftmann |
avoid compound fields in datatype info record
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 09:52:23 +0200 |
haftmann |
registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 00:21:36 +0200 |
wenzelm |
eliminated legacy_varify;
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|