Thu, 03 Apr 2008 16:34:52 +0200 |
krauss |
Function package no longer overwrites theorems.
|
file |
diff |
annotate
|
Wed, 05 Mar 2008 12:24:52 +0100 |
krauss |
Use conversions instead of simplifier. tuned
|
file |
diff |
annotate
|
Fri, 22 Feb 2008 16:48:36 +0100 |
krauss |
removed dead code; some cleanup
|
file |
diff |
annotate
|
Sat, 13 Oct 2007 17:16:39 +0200 |
wenzelm |
renamed LocalTheory.def to LocalTheory.define;
|
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:26 +0200 |
wenzelm |
renamed Syntax.XXX_mode to Syntax.mode_XXX;
|
file |
diff |
annotate
|
Mon, 24 Sep 2007 21:07:38 +0200 |
wenzelm |
eliminated ProofContext.read_termTs;
|
file |
diff |
annotate
|
Sat, 01 Sep 2007 15:47:03 +0200 |
wenzelm |
replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);
|
file |
diff |
annotate
|
Tue, 07 Aug 2007 14:49:58 +0200 |
krauss |
simplified internal interfaces; cong rules are now handled directly by "context_tree.ML"
|
file |
diff |
annotate
|
Fri, 20 Jul 2007 14:28:05 +0200 |
haftmann |
dropped Nat.ML legacy bindings
|
file |
diff |
annotate
|
Mon, 16 Jul 2007 21:22:43 +0200 |
krauss |
some interface cleanup
|
file |
diff |
annotate
|
Wed, 11 Jul 2007 11:46:05 +0200 |
berghofe |
Adapted to changes in Accessible_Part theory.
|
file |
diff |
annotate
|
Fri, 01 Jun 2007 15:57:45 +0200 |
krauss |
simplified interfaces, some restructuring
|
file |
diff |
annotate
|
Mon, 23 Apr 2007 20:44:08 +0200 |
wenzelm |
simplified ProofContext.read_termTs;
|
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
|
Tue, 10 Apr 2007 08:09:28 +0200 |
krauss |
removed obsolete workaround
|
file |
diff |
annotate
|
Thu, 22 Mar 2007 13:36:55 +0100 |
krauss |
cleanup
|
file |
diff |
annotate
|
Fri, 16 Mar 2007 21:32:19 +0100 |
haftmann |
adjusted qualified thm reference
|
file |
diff |
annotate
|
Tue, 06 Mar 2007 15:49:25 +0100 |
krauss |
fixed function package bug in the handling of multiple guards
|
file |
diff |
annotate
|
Thu, 15 Feb 2007 17:35:19 +0100 |
krauss |
changed termination goal to use object quantifier
|
file |
diff |
annotate
|
Wed, 07 Feb 2007 18:03:18 +0100 |
berghofe |
Adapted to changes in Accessible_Part and Wellfounded_Recursion theories.
|
file |
diff |
annotate
|
Mon, 22 Jan 2007 17:29:43 +0100 |
krauss |
* Preliminary implementation of tail recursion
|
file |
diff |
annotate
|