| Tue, 26 Sep 2006 17:33:04 +0200 |
krauss |
Changed precedence of "op O" (relation composition) from 60 to 75.
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 13:34:15 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 23:15:24 +0200 |
wenzelm |
* Pure: 'print_theory' now suppresses entities with internal name;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:31:32 +0200 |
haftmann |
Operational Equality
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:40:14 +0200 |
wenzelm |
* Pure: 'class_deps' command visualizes the subclass relation;
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 14:28:47 +0200 |
haftmann |
hid succ, pred in Numeral.thy
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
| Fri, 01 Sep 2006 08:36:51 +0200 |
haftmann |
final syntax for some Isar code generator keywords
|
file |
diff |
annotate
|
| Mon, 14 Aug 2006 11:16:20 +0200 |
chaieb |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 09 Aug 2006 10:59:58 +0200 |
wenzelm |
* ProofContext.prems_limit is now -1 by default;
|
file |
diff |
annotate
|
| Tue, 08 Aug 2006 08:18:59 +0200 |
haftmann |
abandoned equal_list in favor for eq_list
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 15:58:04 +0200 |
chaieb |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 14:57:26 +0200 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Tue, 25 Jul 2006 16:43:31 +0200 |
haftmann |
added notes on class_package.ML and codegen_package.ML
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 23:22:22 +0200 |
ballarin |
Change to algebra method.
|
file |
diff |
annotate
|
| Mon, 17 Jul 2006 01:28:17 +0200 |
webertj |
support for MiniSat proof traces added
|
file |
diff |
annotate
|
| Wed, 12 Jul 2006 21:19:27 +0200 |
wenzelm |
* Isar: ":" (colon) is no longer a symbolic identifier character;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:30 +0200 |
wenzelm |
* Pure: structure Name;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 00:43:54 +0200 |
kleing |
hex and binary numerals (contributed by Rafal Kolanski)
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:26 +0200 |
wenzelm |
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 21:26:26 +0200 |
wenzelm |
Isar: 'print_facts' prints all local facts;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 14:47:01 +0200 |
ballarin |
Method intro_locales replaced by intro_locales and unfold_locales.
|
file |
diff |
annotate
|
| Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
| Thu, 15 Jun 2006 18:28:32 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 17:16:03 +0200 |
berghofe |
Added "evaluation" method.
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 02:04:20 +0200 |
wenzelm |
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 10:05:57 +0200 |
ballarin |
Improved parameter management of locales.
|
file |
diff |
annotate
|
| Wed, 24 May 2006 22:15:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 24 May 2006 22:13:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 24 May 2006 21:58:07 +0200 |
wenzelm |
Pure: update on overloaded defs;
|
file |
diff |
annotate
|
| Wed, 17 May 2006 22:36:08 +0200 |
wenzelm |
* Pure: syntax 'CONST name' produces a fully internalized constant;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:23 +0200 |
wenzelm |
* Isar/locale: 'const_syntax';
|
file |
diff |
annotate
|
| Tue, 16 May 2006 18:31:46 +0200 |
wenzelm |
* Pure/library: divide_and_conquer;
|
file |
diff |
annotate
|
| Sat, 13 May 2006 02:51:30 +0200 |
wenzelm |
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
|
file |
diff |
annotate
|
| Sun, 07 May 2006 00:47:07 +0200 |
wenzelm |
* Isar: removed obsolete 'concl is' patterns.
|
file |
diff |
annotate
|
| Fri, 05 May 2006 21:59:39 +0200 |
wenzelm |
* Library: theory Accessible_Part has been move to main HOL.
|
file |
diff |
annotate
|
| Sun, 30 Apr 2006 22:49:59 +0200 |
wenzelm |
* Pure: axclasses now purely definitional;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 14:31:37 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 10:04:27 +0100 |
ballarin |
Renamed setsum_mult to setsum_right_distrib.
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 09:34:23 +0100 |
haftmann |
renamed op < <= to Orderings.less(_eq)
|
file |
diff |
annotate
|
| Tue, 14 Mar 2006 22:06:29 +0100 |
wenzelm |
print_statement;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2006 16:29:29 +0100 |
wenzelm |
Pure: no_translations;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2006 10:41:04 +0100 |
schirmer |
entry for Library/AssocList
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 19:49:58 +0100 |
wenzelm |
tuned;
|
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
|
| Wed, 08 Mar 2006 21:40:46 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2006 18:37:25 +0100 |
wenzelm |
Isar/method: goal restriction;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2006 10:06:31 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 21:15:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 19:39:02 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 19:10:47 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 18:39:48 +0100 |
wenzelm |
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:28 +0100 |
wenzelm |
* ML/Pure/General: improved join interface for tables;
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 10 Feb 2006 02:22:57 +0100 |
wenzelm |
* ML/Pure: generic Args/Attrib syntax everywhere;
|
file |
diff |
annotate
|
| Wed, 08 Feb 2006 15:17:54 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 16:37:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 16:31:28 +0100 |
wenzelm |
* Isar: 'obtains' element;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2006 00:51:15 +0100 |
wenzelm |
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:28:48 +0100 |
wenzelm |
Pure/Isar: (un)folded, (un)fold, unfolding support
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:07:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:30 +0100 |
wenzelm |
* ML: simplified type attribute;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:27 +0100 |
wenzelm |
* ML/Isar: theory setup has type (theory -> theory);
|
file |
diff |
annotate
|
| Sun, 15 Jan 2006 20:04:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2006 20:00:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2006 19:58:57 +0100 |
wenzelm |
* Classical: optional weight for attributes;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:20:51 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:15:24 +0100 |
wenzelm |
* ML/Isar: simplified treatment of user-level errors;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 14:43:09 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:36:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:33:42 +0100 |
wenzelm |
* ML: generic context, data, attributes;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 12:26:23 +0100 |
wenzelm |
* Provers/induct: improved simultaneous goals -- nested cases;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2006 15:18:19 +0100 |
wenzelm |
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 01:04:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 01:00:52 +0100 |
wenzelm |
* Pure/Isar: Toplevel.theory_theory_to_proof;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 15:44:39 +0100 |
paulson |
Provers/classical: stricter checks to ensure that supplied intro, dest and
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 11:31:15 +0100 |
haftmann |
rearranged burrow_split to fold_burrow to allow composition with fold_map
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 00:06:18 +0100 |
wenzelm |
* Pure/Isar: new command 'unfolding';
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:44 +0100 |
wenzelm |
* Provers/classical: removed obsolete classical version of elim_format;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:21:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:18:13 +0100 |
wenzelm |
* Provers/induct: support simultaneous goals with mutual rules;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 14:33:28 +0100 |
haftmann |
is_prefix
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:41:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:12 +0100 |
wenzelm |
* induct: improved treatment of mutual goals and mutual rules;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 13:25:20 +0100 |
haftmann |
discontinued unflat in favour of burrow and burrow_split
|
file |
diff |
annotate
|
| Tue, 20 Dec 2005 22:06:00 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2005 16:00:58 +0100 |
haftmann |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
file |
diff |
annotate
|
| Tue, 13 Dec 2005 19:32:06 +0100 |
wenzelm |
Provers/induct: coinduct;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 20:15:34 +0100 |
wenzelm |
removed hint for Classical.swap, which is not really user-level anyway;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 12:50:02 +0100 |
wenzelm |
* HOL: Theorem 'swap' is no longer bound at the ML top-level.
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 22:52:46 +0100 |
wenzelm |
simulaneous 'def';
|
file |
diff |
annotate
|
| Sun, 27 Nov 2005 20:06:24 +0100 |
wenzelm |
* Provers/induct: obtain pattern;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 18:58:34 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 20:29:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 18:52:05 +0100 |
wenzelm |
Provers/induct: definitional insts and fixing;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 18:52:00 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 20:57:11 +0100 |
wenzelm |
renamed Thm.cgoal_of to Thm.cprem_of;
|
file |
diff |
annotate
|
| Mon, 31 Oct 2005 16:35:15 +0100 |
haftmann |
nth_*, fold_index refined
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:37:57 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:27:41 +0200 |
wenzelm |
* Pure/Isar: literal facts;
|
file |
diff |
annotate
|
| Thu, 27 Oct 2005 13:59:06 +0200 |
wenzelm |
* HOL: alternative iff syntax;
|
file |
diff |
annotate
|
| Thu, 27 Oct 2005 08:14:05 +0200 |
haftmann |
added module Pure/General/rat.ML
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:16:57 +0200 |
wenzelm |
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 21:52:30 +0200 |
wenzelm |
* Theory syntax: discontinued non-Isar format and old Isar headers;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:23 +0200 |
wenzelm |
Simplifier.context/theory_context;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:25 +0200 |
wenzelm |
* Simplifier: simpset of a running simplification process contains a proof context;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Oct 2005 00:14:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Oct 2005 00:08:14 +0200 |
wenzelm |
* antiquotations ML_type, ML_struct;
|
file |
diff |
annotate
|
| Sun, 09 Oct 2005 17:06:03 +0200 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
file |
diff |
annotate
|
| Sat, 08 Oct 2005 23:36:01 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 22:59:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 22:59:15 +0200 |
wenzelm |
added dummy variable binding;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 16:47:39 +0200 |
wenzelm |
* Command 'find_theorems': support * wildcard in name: criterion.
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 17:08:52 +0200 |
wenzelm |
pdfsetup.sty: better not rely on ifpdf.sty;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 15:50:43 +0200 |
wenzelm |
Isabelle2005 (October 2005);
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 00:58:54 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 28 Sep 2005 18:50:42 +0200 |
webertj |
pointer to HOL/ex/SAT_Examples.thy added
|
file |
diff |
annotate
|
| Wed, 28 Sep 2005 11:50:13 +0200 |
wenzelm |
revert 'defs' advertisement;
|
file |
diff |
annotate
|
| Tue, 27 Sep 2005 17:24:27 +0200 |
wenzelm |
more details about incomplete 'defs';
|
file |
diff |
annotate
|
| Tue, 27 Sep 2005 11:27:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 27 Sep 2005 11:03:38 +0200 |
berghofe |
Added entries for code_module, code_library, and value.
|
file |
diff |
annotate
|
| Sun, 25 Sep 2005 20:24:23 +0200 |
wenzelm |
* Hyperreal: A theory of Taylor series.
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 23:28:59 +0200 |
webertj |
new sat tactic
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 13:20:47 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 10:25:55 +0200 |
paulson |
ATP linkup
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 00:10:58 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 18:59:41 +0200 |
huffman |
HOLCF theorem naming conventions
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 17:21:35 +0200 |
haftmann |
added AList.make, eq_fst, apr ...
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 11:50:52 +0200 |
wenzelm |
tunes;
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 00:07:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 22:02:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 21:48:47 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:20:58 +0200 |
wenzelm |
HOL/ex/Chinese.thy;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 08:20:22 +0200 |
haftmann |
infix operator precedence
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:17 +0200 |
wenzelm |
HTML.with_charset;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 12:18:00 +0200 |
wenzelm |
Cube: converted to Isar, use locales;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 23:55:23 +0200 |
huffman |
add HOLCF entries for pcpodef, cont_proc, fixrec;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 14:44:52 +0200 |
ballarin |
tuned
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 20:27:48 +0200 |
wenzelm |
* Improved efficiency of the Simplifier etc.;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 20:24:53 +0200 |
wenzelm |
incorporated HOL/Hyperreal/CHANGES;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:53 +0200 |
wenzelm |
command 'thms_containing' has been discontinued in favour of 'find_theorems';
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 10:00:01 +0200 |
haftmann |
AList, the_*
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 23:31:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 23:15:00 +0200 |
wenzelm |
hide: added option '(open)';
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 23:06:02 +0200 |
schirmer |
... prem19
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 22:18:55 +0200 |
wenzelm |
Method comm_ring for proving equalities in commutative rings.
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 22:04:36 +0200 |
wenzelm |
HOL: method comm_ring;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:49:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 16:59:50 +0200 |
wenzelm |
axclass: name space prefix is now "c_class" instead of just "c";
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 17:49:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 17:38:15 +0200 |
wenzelm |
Markup commands 'chapter' .. 'text' support optional locale specification;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 09:50:58 +0200 |
ballarin |
print_locale omits facts by default
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:30 +0200 |
wenzelm |
* Delimiters of outer tokens now produce separate LaTeX macros;
|
file |
diff |
annotate
|
| Tue, 30 Aug 2005 12:47:53 +0200 |
paulson |
patterns in setsum and setprod
|
file |
diff |
annotate
|
| Sun, 28 Aug 2005 16:06:07 +0200 |
wenzelm |
* ML functions legacy_bindings and use_legacy_bindings;
|
file |
diff |
annotate
|
| Sun, 28 Aug 2005 16:04:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2005 12:07:00 +0200 |
ballarin |
Printing of interpretations: option to show witness theorems;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2005 11:59:17 +0200 |
wenzelm |
* The ML antiquotation prints type-checked ML expressions verbatim.
|
file |
diff |
annotate
|
| Thu, 18 Aug 2005 11:17:32 +0200 |
wenzelm |
* Proper output of proof terms within a proof context;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2005 17:03:20 +0200 |
ballarin |
Interpretation in locales.
|
file |
diff |
annotate
|
| Wed, 17 Aug 2005 14:19:17 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:42:13 +0200 |
wenzelm |
* Command tags control specific markup of certain regions of text (replaces usedir -H);
|
file |
diff |
annotate
|
| Wed, 03 Aug 2005 14:49:04 +0200 |
avigad |
mentioned change to exp_ge_add_one_self, new transitivity rules
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:21:38 +0200 |
wenzelm |
* Pure/Simplifier: improved handling of bound variables;
|
file |
diff |
annotate
|
| Fri, 29 Jul 2005 19:47:41 +0200 |
avigad |
mentioned Ln in NEWS
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:19:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 25 Jul 2005 18:54:49 +0200 |
avigad |
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 17:54:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 17:24:09 +0200 |
avigad |
added list of theorem changes to NEWS
|
file |
diff |
annotate
|
| Mon, 18 Jul 2005 14:10:11 +0200 |
haftmann |
reverted from fold_yield to fold_map
|
file |
diff |
annotate
|
| Fri, 15 Jul 2005 15:45:04 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 15 Jul 2005 15:44:11 +0200 |
wenzelm |
* Pure/library.ML: several combinators for linear functional transformations;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:29:00 +0200 |
wenzelm |
* Improved 'oracle' command -- type-safe;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:18 +0200 |
wenzelm |
* Isar session: The initial use of ROOT.ML is now always timed;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2005 20:00:20 +0200 |
wenzelm |
* Pure: Output.time_accumulator;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2005 10:41:51 +0200 |
wenzelm |
isatool fixheaders;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2005 15:39:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2005 14:07:08 +0200 |
wenzelm |
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 14:55:05 +0200 |
wenzelm |
* Isar profiling: new reference Toplevel.profiling (default 0);
|
file |
diff |
annotate
|
| Fri, 24 Jun 2005 17:25:10 +0200 |
paulson |
meson method taking an argument list
|
file |
diff |
annotate
|
| Wed, 22 Jun 2005 19:48:20 +0200 |
wenzelm |
* Pure: the Isar proof context type is already defined early in Pure
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:14:21 +0200 |
wenzelm |
* Pure: get_thm interface expects datatype thmref;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:41 +0200 |
wenzelm |
* Pure/TheoryDataFun: change of the argument structure;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2005 22:15:58 +0200 |
wenzelm |
* Pure/sign/theory: discontinued named name spaces;
|
file |
diff |
annotate
|
| Sun, 05 Jun 2005 11:31:14 +0200 |
wenzelm |
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
|
file |
diff |
annotate
|
| Sat, 04 Jun 2005 18:20:00 +0200 |
wenzelm |
major reorganization and cleanup;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2005 09:12:56 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 01 Jun 2005 12:30:49 +0200 |
ballarin |
Locales: new element constrains, parameter renaming with syntax,
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:42 +0200 |
wenzelm |
ML Pure: name spaces have been refined;
|
file |
diff |
annotate
|
| Mon, 30 May 2005 10:25:46 +0200 |
kleing |
typo
|
file |
diff |
annotate
|
| Mon, 30 May 2005 10:23:15 +0200 |
kleing |
updated para on searching
|
file |
diff |
annotate
|
| Fri, 27 May 2005 17:10:23 +0200 |
ballarin |
Typo.
|
file |
diff |
annotate
|
| Fri, 27 May 2005 16:24:48 +0200 |
ballarin |
Locale expressions: rename with optional mixfix syntax.
|
file |
diff |
annotate
|
| Mon, 23 May 2005 19:14:16 +0200 |
wenzelm |
* Pure/Syntax: In schematic variable names, *any* symbol following
|
file |
diff |
annotate
|
| Mon, 23 May 2005 11:14:58 +0200 |
nipkow |
tuned trace info (depth)
|
file |
diff |
annotate
|
| Sun, 22 May 2005 16:51:02 +0200 |
wenzelm |
removed find_rewrites (superceded by improved thms_containing);
|
file |
diff |
annotate
|
| Wed, 18 May 2005 10:51:15 +0200 |
kleing |
searching for combination of criteria (intro, elim, dest, name, pattern)
|
file |
diff |
annotate
|
| Tue, 17 May 2005 18:10:31 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 17 May 2005 10:19:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 06 May 2005 08:37:39 +0200 |
haftmann |
added new antiquotations
|
file |
diff |
annotate
|
| Fri, 29 Apr 2005 11:40:29 +0200 |
kleing |
new thms_containing that searches for patterns instead of constants
|
file |
diff |
annotate
|
| Tue, 26 Apr 2005 19:53:19 +0200 |
wenzelm |
allow symlinks to all proper Isabelle executables;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2005 14:18:33 +0200 |
gagern |
Allow symlinks to shell scripts
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 18:46:04 +0200 |
webertj |
refute extended
|
file |
diff |
annotate
|
| Mon, 18 Apr 2005 09:25:23 +0200 |
ballarin |
Interpretation supports statically scoped attributes; documentation.
|
file |
diff |
annotate
|
| Sat, 16 Apr 2005 18:55:28 +0200 |
wenzelm |
Pure: command 'no_syntax' removes grammar declarations;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 20:20:14 +0200 |
wenzelm |
Locales: proper static binding of attribute syntax;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:50:08 +0200 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:34:22 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 11 Apr 2005 12:34:34 +0200 |
ballarin |
First release of interpretation commands.
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 14:07:40 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Wed, 16 Feb 2005 19:00:49 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Fri, 11 Feb 2005 10:03:41 +0100 |
ballarin |
New reference Toplevel.debug for verbose printing of exns.
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Fri, 28 Jan 2005 04:34:55 +0100 |
kleing |
-H false for showing proofs (not -H true)
|
file |
diff |
annotate
|
| Thu, 27 Jan 2005 12:37:02 +0100 |
berghofe |
- Proofs are now hidden by default when generating documents
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 12:41:06 +0100 |
paulson |
thin_tac now works on P==>Q
|
file |
diff |
annotate
|
| Tue, 11 Jan 2005 14:20:45 +0100 |
berghofe |
Option for hiding proof scripts in documents.
|
file |
diff |
annotate
|
| Sat, 18 Dec 2004 17:14:33 +0100 |
schirmer |
added simproc for Let
|
file |
diff |
annotate
|
| Mon, 13 Dec 2004 17:44:52 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 02 Dec 2004 11:44:55 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 01 Dec 2004 18:17:01 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 01 Dec 2004 06:33:52 +0100 |
kleing |
new antiquotations @{lhs thm} and @{rhs thm}
|
file |
diff |
annotate
|
| Wed, 24 Nov 2004 08:43:41 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 15 Nov 2004 17:04:11 +0100 |
webertj |
minor rewording
|
file |
diff |
annotate
|
| Fri, 12 Nov 2004 15:45:19 +0100 |
webertj |
isatool usedir -f
|
file |
diff |
annotate
|
| Tue, 12 Oct 2004 16:59:56 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 27 Sep 2004 10:27:34 +0200 |
ballarin |
Modified locales: improved implementation of "includes".
|
file |
diff |
annotate
|
| Mon, 13 Sep 2004 09:57:25 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sun, 29 Aug 2004 17:42:11 +0200 |
webertj |
Provers/blast.ML: depth_limit
|
file |
diff |
annotate
|
| Mon, 23 Aug 2004 16:41:06 +0200 |
webertj |
new isatool dimacs2hol
|
file |
diff |
annotate
|
| Thu, 19 Aug 2004 10:33:10 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:21:54 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|