| Wed, 25 Mar 2009 14:47:08 +0100 |
wenzelm |
avoid mixing of left/right associative infixes, to make it work with experimental Poly/ML 5.3 branch;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 20:25:58 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 15:50:06 +0100 |
wenzelm |
provide regular ML interfaces for Isar source language elements;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:23:11 +0100 |
haftmann |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file |
diff |
annotate
|
| Mon, 02 Feb 2009 15:12:22 +0100 |
krauss |
export lexicographic_order_tac
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 12:13:50 +0200 |
krauss |
termination prover for "fun" can be configured using context data.
|
file |
diff |
annotate
|
| Fri, 08 Aug 2008 09:44:16 +0200 |
krauss |
FundefLib.try_proof : attempt a proof and see if it works
|
file |
diff |
annotate
|
| Mon, 04 Aug 2008 18:24:27 +0200 |
krauss |
removed dead code
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:39 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
| Mon, 12 May 2008 22:11:06 +0200 |
krauss |
Measure functions can now be declared via special rules, allowing for a
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 16:28:06 +0200 |
krauss |
* New attribute "termination_simp": Simp rules for termination proofs
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
| Thu, 03 Apr 2008 16:34:52 +0200 |
krauss |
Function package no longer overwrites theorems.
|
file |
diff |
annotate
|
| 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
|