| Wed, 05 Dec 2007 14:36:58 +0100 |
krauss |
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:16:05 +0100 |
haftmann |
map_product and fold_product
|
file |
diff |
annotate
|
| Fri, 30 Nov 2007 16:23:52 +0100 |
krauss |
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 19:10:19 +0200 |
wenzelm |
replaced (flip Thm.implies_elim) by Thm.elim_implies;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 16:05:30 +0200 |
wenzelm |
moved ProofContext.pp to Syntax.pp;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Fri, 14 Sep 2007 22:22:53 +0200 |
krauss |
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:28:25 +0200 |
haftmann |
moved class ord from Orderings.thy to HOL.thy
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 18:39:12 +0200 |
wenzelm |
pr_goals: adapted Display.pretty_goals_aux;
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 17:02:57 +0200 |
krauss |
tuned error msg
|
file |
diff |
annotate
|
| Wed, 30 May 2007 18:05:10 +0200 |
krauss |
clarified error message
|
file |
diff |
annotate
|
| Tue, 22 May 2007 17:25:26 +0200 |
krauss |
some optimizations, cleanup
|
file |
diff |
annotate
|
| Mon, 21 May 2007 16:39:58 +0200 |
krauss |
fixed signature
|
file |
diff |
annotate
|
| Mon, 21 May 2007 16:22:46 +0200 |
krauss |
Method "lexicographic_order" now takes the same arguments as "auto"
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:40 +0200 |
haftmann |
canonical prefixing of class constants
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 10:06:11 +0200 |
krauss |
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
|
file |
diff |
annotate
|
| Thu, 15 Feb 2007 17:35:19 +0100 |
krauss |
changed termination goal to use object quantifier
|
file |
diff |
annotate
|
| Tue, 13 Feb 2007 10:09:21 +0100 |
bulwahn |
improved lexicographic order termination tactic
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 13:05:28 +0100 |
bulwahn |
changes in lexicographic_order termination tactic
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 14:56:50 +0100 |
krauss |
clarified error message
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 14:54:07 +0100 |
krauss |
nat type now has a size functin => no longer needed as special case
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 19:37:28 +0100 |
wenzelm |
HOLogic cleanup;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:57 +0100 |
wenzelm |
tuned spaces/comments;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 13:39:22 +0100 |
krauss |
exported mk_base_funs for use by size-change tools
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 13:51:22 +0100 |
krauss |
replaced "auto_term" by the simpler method "relation", which does not try
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 22:06:32 +0100 |
krauss |
untabified
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 09:59:43 +0100 |
krauss |
method exported
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 08:46:54 +0100 |
bulwahn |
added lexicographic_order tactic
|
file |
diff |
annotate
|