| Tue, 18 Sep 2007 08:28:47 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sun, 16 Sep 2007 21:04:43 +0200 |
wenzelm |
moved induct patterns to HOL/Induct/Common_Patterns.thy;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 01:22:11 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 31 Aug 2007 16:17:53 +0200 |
wenzelm |
tuned multithreading entry -- no longer experimental;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 21:44:29 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:18 +0200 |
haftmann |
moved class dense_linear_order to Orderings.thy
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:07:25 +0200 |
haftmann |
conciliated Inf/Inf_fin
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 04:34:31 +0200 |
kleing |
* HOL-Word:
|
file |
diff |
annotate
|
| Mon, 13 Aug 2007 04:35:41 +0200 |
kleing |
new attribute [rotated]
|
file |
diff |
annotate
|
| Sun, 12 Aug 2007 19:00:58 +0200 |
wenzelm |
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 11:02:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 00:20:39 +0200 |
wenzelm |
* Experimental support for multithreading, using Poly/ML 5.1;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2007 23:07:46 +0200 |
wenzelm |
* Theory loader: old-style ML proof scripts are considered a legacy feature;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 20:19:48 +0200 |
wenzelm |
theory loader: added use_thys, removed obsolete update_thy;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2007 16:55:37 +0200 |
wenzelm |
tuned config options: eliminated separate attribute "option";
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 13:31:01 +0200 |
wenzelm |
* Configuration options;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 22:17:46 +0200 |
wenzelm |
* Isar: command 'declaration';
|
file |
diff |
annotate
|
| Wed, 25 Jul 2007 10:19:01 +0200 |
ballarin |
tuned
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 21:51:18 +0200 |
krauss |
renamed lemma "set_take_whileD" to "set_takeWhileD"
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 13:50:31 +0200 |
ballarin |
interpretation: unfolding of equations;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 19:13:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 19:10:05 +0200 |
wenzelm |
* Theory loader: be more serious about observing the static theory header specifications;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:28:25 +0200 |
haftmann |
moved class ord from Orderings.thy to HOL.thy
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:34 +0200 |
haftmann |
updated
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 12:23:34 +0200 |
berghofe |
Added entry for new inductive definition package.
|
file |
diff |
annotate
|
| Wed, 04 Jul 2007 14:21:00 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 04 Jul 2007 14:10:01 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 23:00:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 27 Jun 2007 11:06:43 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 14:49:32 +0200 |
obua |
commented changes in HOL/Ring_and_Field.thy, and in HOL/Real/RealPow.thy
|
file |
diff |
annotate
|
| Sun, 24 Jun 2007 20:47:05 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sun, 24 Jun 2007 20:18:20 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sun, 24 Jun 2007 10:33:49 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 22:30:58 +0200 |
huffman |
changed simp rules for of_nat
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 13:23:33 +0200 |
paulson |
integration of Metis prover
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 00:48:42 +0200 |
wenzelm |
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 19:14:51 +0200 |
huffman |
int abbreviates of_nat
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 11:54:03 +0200 |
wenzelm |
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 10:44:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 10 Jun 2007 10:23:42 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 08 Jun 2007 18:09:37 +0200 |
chaieb |
Method "algebra" solves polynomial equations over (semi)rings
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 15:17:02 +0200 |
haftmann |
moved generic algebra modules
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 13:19:03 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 01 Jun 2007 10:44:24 +0200 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
| Wed, 30 May 2007 21:09:09 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 28 May 2007 16:30:28 +0200 |
huffman |
Complex: generalized type of exp
|
file |
diff |
annotate
|
| Fri, 25 May 2007 18:24:11 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 25 May 2007 18:11:25 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 25 May 2007 18:10:56 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sat, 19 May 2007 11:33:57 +0200 |
haftmann |
constant op @ now named append
|
file |
diff |
annotate
|
| Sat, 19 May 2007 07:47:51 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 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
|