Wed, 21 Oct 2009 08:16:25 +0200 |
haftmann |
merged
|
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
|
Tue, 20 Oct 2009 20:54:31 +0200 |
wenzelm |
uniform use of Integer.min/max;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 21:14:08 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 20:37:38 +0200 |
wenzelm |
removed separate record_quick_and_dirty_sensitive;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 20:15:59 +0200 |
wenzelm |
simplified tactics;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 19:04:35 +0200 |
wenzelm |
eliminated old List.foldr and OldTerm operations;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 18:14:47 +0200 |
wenzelm |
removed unused names;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 18:01:24 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 16:58:03 +0200 |
wenzelm |
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 00:52:37 +0200 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
Thu, 01 Oct 2009 14:11:28 +0200 |
wenzelm |
avoid mixed l/r infixes, which do not work in some versions of SML;
|
file |
diff |
annotate
|
Thu, 01 Oct 2009 12:15:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 01 Oct 2009 01:03:36 +0200 |
wenzelm |
eliminated dead code, redundant bindings and parameters;
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 00:27:19 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 23:14:57 +0200 |
wenzelm |
removed dead/duplicate code;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 22:48:24 +0200 |
wenzelm |
modernized Balanced_Tree;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 22:33:27 +0200 |
wenzelm |
replaced meta_iffD2 by existing Drule.equal_elim_rule2;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 21:36:49 +0200 |
wenzelm |
tuned header;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 21:34:59 +0200 |
wenzelm |
tuned whitespace -- recover basic Isabelle conventions;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 18:14:08 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 14:25:42 +1000 |
Thomas Sewell |
Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.
|
file |
diff |
annotate
|
Mon, 28 Sep 2009 15:37:19 +1000 |
Thomas Sewell |
Avoid a possible variable name conflict in instantiating a theorem.
|
file |
diff |
annotate
|
Wed, 23 Sep 2009 19:17:48 +1000 |
tsewell |
Initial response to feedback from Norbert, Makarius on record patch
|
file |
diff |
annotate
|
Fri, 11 Sep 2009 20:58:29 +1000 |
Thomas Sewell |
Implement previous fix (don't duplicate ext_def) correctly.
|
file |
diff |
annotate
|
Fri, 11 Sep 2009 18:03:30 +1000 |
Thomas Sewell |
There's no particular reason to duplicate the extension
|
file |
diff |
annotate
|
Thu, 10 Sep 2009 16:38:18 +1000 |
Thomas Sewell |
Simplification of various aspects of the IsTuple component
|
file |
diff |
annotate
|
Thu, 10 Sep 2009 15:18:43 +1000 |
Thomas Sewell |
Record patch imported and working.
|
file |
diff |
annotate
|