| Tue, 14 Feb 2012 20:08:59 +0100 |
comment;
|
file | diff | annotate |
| Sat, 14 Jan 2012 19:06:05 +0100 |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
file | diff | annotate |
| Wed, 27 Apr 2011 21:50:04 +0200 |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
file | diff | annotate |
| Sat, 16 Apr 2011 16:15:37 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Wed, 29 Dec 2010 21:52:44 +0100 |
more robust decomposition of simultaneous goals
|
file | diff | annotate |
| Fri, 17 Dec 2010 17:08:56 +0100 |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file | diff | annotate |
| Fri, 17 Dec 2010 13:45:43 +0100 |
refer to regular structure Simplifier;
|
file | diff | annotate |
| Mon, 13 Dec 2010 10:15:27 +0100 |
eliminated dest_all_all_ctx
|
file | diff | annotate |
| Tue, 28 Sep 2010 12:34:41 +0200 |
consolidated tupled_lambda; moved to structure HOLogic
|
file | diff | annotate |
| Thu, 01 Jul 2010 16:54:42 +0200 |
qualified constants Set.member and Set.Collect
|
file | diff | annotate |
| Sat, 15 May 2010 21:50:05 +0200 |
less pervasive names from structure Thm;
|
file | diff | annotate |
| Sun, 07 Mar 2010 12:19:47 +0100 |
modernized structure Object_Logic;
|
file | diff | annotate |
| Sat, 02 Jan 2010 23:18:58 +0100 |
new year's resolution: reindented code in function package
|
file | diff | annotate |
| Mon, 23 Nov 2009 15:05:59 +0100 |
eliminated dead code and some unused bindings, reported by polyml
|
file | diff | annotate |
| Sun, 15 Nov 2009 15:14:28 +0100 |
tuned;
|
file | diff | annotate |
| Fri, 06 Nov 2009 14:42:42 +0100 |
renamed method induct_scheme to induction_schema
|
file | diff | annotate |