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