Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
Fri, 12 Oct 2007 08:25:48 +0200 |
haftmann |
moved class power to theory Power
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 16:08:00 +0200 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 19:19:30 +0200 |
haftmann |
tuned integers
|
file |
diff |
annotate
|
Thu, 17 May 2007 19:49:40 +0200 |
haftmann |
canonical prefixing of class constants
|
file |
diff |
annotate
|
Mon, 14 May 2007 12:52:54 +0200 |
haftmann |
fixed IntInf ambiguity
|
file |
diff |
annotate
|
Sun, 13 May 2007 18:15:25 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
Tue, 26 Sep 2006 13:34:16 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 23:15:30 +0200 |
wenzelm |
tuned method setup;
|
file |
diff |
annotate
|
Fri, 10 Mar 2006 15:33:48 +0100 |
haftmann |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
file |
diff |
annotate
|
Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
Tue, 20 Sep 2005 14:10:29 +0200 |
wenzelm |
added Commutative_Ring (from Main HOL);
|
file |
diff |
annotate
|