| Tue, 17 Apr 2012 11:03:08 +0200 |
huffman |
add theory data for relator identity rules;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 16:05:52 +0200 |
huffman |
transfer method generalizes over free variables in goal
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 16:03:01 +0200 |
huffman |
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 07:47:42 +0200 |
huffman |
add type annotations to make SML happy (cf. ec6187036495)
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 22:31:00 +0200 |
huffman |
new transfer proof method
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
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
|
| Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 21:36:18 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:56:33 +0100 |
haftmann |
meaningful transfer certificate
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 09:09:43 +0100 |
haftmann |
made smlnj happy
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 21:19:49 +0100 |
haftmann |
clarified transfer code proper; more natural declaration of return rules
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 18:31:37 +0100 |
haftmann |
data administration using canonical functorial operations
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 16:15:19 +0100 |
haftmann |
tuned data structures; using AList.map_default
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 15:47:16 +0100 |
haftmann |
consistent field names; tuned interface
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 14:41:56 +0100 |
haftmann |
proper ML interface; further polishing
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 13:22:41 +0100 |
haftmann |
code simplification and tuning
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 09:38:59 +0100 |
haftmann |
transfer: avoid camel case, more standard coding conventions, misc tuning
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 08:46:12 +0100 |
haftmann |
dropped dead code; adhere more closely to standard coding conventions
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:39 +0100 |
haftmann |
join entries properly on theory merge
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:02:56 +0200 |
haftmann |
curried union as canonical list operation
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 16:09:47 +0200 |
wenzelm |
handle Pattern.MATCH, not arbitrary exceptions;
|
file |
diff |
annotate
|
| Thu, 10 Sep 2009 15:23:09 +0200 |
haftmann |
plain structure name; signature constraint; shorter lines
|
file |
diff |
annotate
| base
|