| Tue, 01 Jun 2010 11:30:57 +0200 |
merged
|
file | diff | annotate |
| Tue, 01 Jun 2010 11:13:09 +0200 |
Adapted to new format of proof terms containing explicit proofs of class membership.
|
file | diff | annotate |
| Wed, 26 May 2010 16:05:25 +0200 |
dropped legacy theorem bindings
|
file | diff | annotate |
| Sat, 08 May 2010 16:53:53 +0200 |
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 |
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 |
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 |
modernized structure Object_Logic;
|
file | diff | annotate |
| Thu, 25 Feb 2010 22:32:09 +0100 |
more antiquotations;
|
file | diff | annotate |
| Mon, 30 Nov 2009 12:28:12 +0100 |
dropped some unused bindings
|
file | diff | annotate |
| Mon, 30 Nov 2009 11:42:49 +0100 |
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 |
eliminated some old folds;
|
file | diff | annotate |
| Wed, 21 Oct 2009 00:36:12 +0200 |
standardized basic operations on type option;
|
file | diff | annotate |
| Thu, 15 Oct 2009 23:28:10 +0200 |
replaced String.concat by implode;
|
file | diff | annotate |
| Mon, 28 Sep 2009 10:20:21 +0200 |
avoid compound fields in datatype info record
|
file | diff | annotate |
| Sun, 27 Sep 2009 09:52:23 +0200 |
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 |
eliminated legacy_varify;
|
file | diff | annotate |
| Tue, 23 Jun 2009 16:27:12 +0200 |
tuned interfaces of datatype module
|
file | diff | annotate |
| Tue, 23 Jun 2009 12:09:30 +0200 |
uniformly capitialized names for subdirectories
|
file | diff | annotate | base |