| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 15:12:03 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
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
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 15:37:37 +0200 |
wenzelm |
more tight name invention -- avoiding old functions;
|
file |
diff |
annotate
|
| Thu, 03 Jun 2010 23:56:05 +0200 |
wenzelm |
do not open Proofterm, which is very ould style;
|
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
|
| 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
|
| Tue, 30 Mar 2010 15:25:30 +0200 |
krauss |
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 21:57:16 +0100 |
wenzelm |
generalized procs for rewrite_proof: allow skeleton;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Sat, 15 Nov 2008 21:31:29 +0100 |
wenzelm |
rewrite_proof: simplified simprocs (no name required);
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:09 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 16:40:16 +0200 |
haftmann |
canonical merge operations
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 18:04:44 +0100 |
berghofe |
Added functions hhf_proof and un_hhf_proof.
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:01 +0200 |
wenzelm |
Name.invent_list;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Wed, 26 Apr 2006 22:38:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 25 Apr 2006 22:23:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:20 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Wed, 22 Feb 2006 22:18:41 +0100 |
wenzelm |
rew: handle conjunctionI/D1/D2;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:31 +0100 |
wenzelm |
Term.betapplys;
|
file |
diff |
annotate
|