| Thu, 17 May 2007 19:49:40 +0200 |
haftmann |
canonical prefixing of class constants
|
file |
diff |
annotate
|
| Mon, 14 May 2007 20:14:31 +0200 |
huffman |
generalized sgn function to work on any real normed vector space
|
file |
diff |
annotate
|
| Mon, 14 May 2007 19:14:50 +0200 |
huffman |
root and sqrt on negative inputs
|
file |
diff |
annotate
|
| Mon, 14 May 2007 13:24:22 +0200 |
webertj |
ProofGeneral: Find Theorems search form
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:22:17 +0200 |
haftmann |
consts in consts_code Isar commands are now referred to by usual term syntax
|
file |
diff |
annotate
|
| Tue, 08 May 2007 17:40:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 08 May 2007 15:01:28 +0200 |
wenzelm |
tuned context data;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:52:25 +0200 |
wenzelm |
* Context data interfaces;
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Mon, 30 Apr 2007 13:32:58 +0200 |
wenzelm |
explicit treatment of legacy_features;
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:32:59 +0200 |
haftmann |
moved code generation pretty integers and characters to separate theories
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 15:13:06 +0200 |
haftmann |
clarifed
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:33 +0200 |
haftmann |
code generator changes
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 21:32:06 +0100 |
haftmann |
lattice cleanup
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
| Fri, 02 Mar 2007 15:43:15 +0100 |
haftmann |
prefix of class interpretation not mandatory any longer
|
file |
diff |
annotate
|
| Wed, 28 Feb 2007 22:05:41 +0100 |
wenzelm |
added @{const_name}, @{const_syntax};
|
file |
diff |
annotate
|
| Wed, 14 Feb 2007 10:06:12 +0100 |
haftmann |
added class "preorder"
|
file |
diff |
annotate
|
| Wed, 31 Jan 2007 16:05:10 +0100 |
haftmann |
dropped lemma duplicates in HOL.thy
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 19:09:35 +0100 |
wenzelm |
* ML in Isar: improved error reporting;
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 17:13:30 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:09:23 +0100 |
wenzelm |
* ML within Isar: antiquotations;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:31:17 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:14:23 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 12:38:51 +0100 |
wenzelm |
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
|
file |
diff |
annotate
|
| Fri, 22 Dec 2006 14:03:30 +0100 |
ballarin |
Experimenting with interpretations of "definition".
|
file |
diff |
annotate
|
| Mon, 18 Dec 2006 08:21:35 +0100 |
haftmann |
switched argument order in *.syntax lifters
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 17:15:42 +0100 |
huffman |
additions to HOL-Complex
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 15:30:31 +0100 |
wenzelm |
added print_abbrevs;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2006 18:05:36 +0100 |
wenzelm |
added antiquotation abbrev;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:42:36 +0100 |
wenzelm |
* Pure: official theorem names and additional comments are now strictly separate.
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:47:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:30 +0100 |
haftmann |
adjusted syntax for internal code generation
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:36 +0100 |
wenzelm |
* Pure: syntax constant for foo (binder) is called foo_binder;
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 20:51:00 +0100 |
wenzelm |
* settings: ML_IDENTIFIER includes the Isabelle version identifier;
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 10:21:17 +0100 |
haftmann |
added Isar syntax for adding parameters to axclasses
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 20:47:58 +0100 |
wenzelm |
* Isar: the assumptions of a long theorem statement are available as assms;
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:12 +0100 |
haftmann |
adjustments for class package
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 15:29:50 +0100 |
wenzelm |
tuned antiquotation theory;
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 20:08:52 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 15:43:24 +0100 |
haftmann |
added antiquotation theory
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 13:53:48 +0100 |
krauss |
updated
|
file |
diff |
annotate
|
| Sat, 11 Nov 2006 16:12:23 +0100 |
wenzelm |
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 11:58:51 +0100 |
wenzelm |
HOL: less/less_eq on bool, modified syntax;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 23:11:13 +0100 |
wenzelm |
moved theories Parity, GCD, Binomial to Library;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 11:22:40 +0100 |
wenzelm |
moved contribution note to CONTRIBUTORS;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 09:08:54 +0100 |
krauss |
Made "termination by lexicographic_order" the default for "fun" definitions.
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 18:25:48 +0100 |
schirmer |
field-update in records is generalised to take a function on the field
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 14:03:04 +0100 |
haftmann |
made locale partial_order compatible with axclass order
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:56 +0100 |
wenzelm |
'const_syntax' command: allow fixed variables, renamed to 'notation';
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 09:41:14 +0100 |
krauss |
updated NEWS
|
file |
diff |
annotate
|
| Sat, 04 Nov 2006 19:25:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 14:58:12 +0100 |
haftmann |
adapted to new serializer syntax
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:28:52 +0100 |
haftmann |
dropped nth_update
|
file |
diff |
annotate
|
| Mon, 23 Oct 2006 16:56:35 +0200 |
haftmann |
(added entry)
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 10:44:33 +0200 |
haftmann |
Symtab.foldl replaced by Symtab.fold
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 10:27:54 +0200 |
ballarin |
Order and lattice structures no longer based on records.
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 22:59:36 +0200 |
wenzelm |
* isabelle-process: option -S (secure mode) disables some critical operations;
|
file |
diff |
annotate
|
| Tue, 10 Oct 2006 13:59:13 +0200 |
haftmann |
gen_rem(s) abandoned in favour of remove / subtract
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 12:08:33 +0200 |
wenzelm |
attribute "symmetric": standardized schematic variables;
|
file |
diff |
annotate
|
| Wed, 04 Oct 2006 14:25:47 +0200 |
haftmann |
insert replacing ins ins_int ins_string
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 18:29:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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
|