| Fri, 17 Apr 2015 17:49:19 +0200 |
wenzelm |
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
|
file |
diff |
annotate
|
| Fri, 17 Apr 2015 15:54:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Apr 2015 14:57:25 +0200 |
wenzelm |
tuned for release;
|
file |
diff |
annotate
|
| Fri, 17 Apr 2015 13:01:09 +0200 |
traytel |
(low importance) NEWS
|
file |
diff |
annotate
|
| Fri, 17 Apr 2015 11:28:57 +0200 |
wenzelm |
allow to exclude session groups;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 14:18:32 +0200 |
wenzelm |
explicit error for Toplevel.proof_of;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 13:48:10 +0200 |
wenzelm |
clarified thy_deps;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 11:22:36 +0200 |
wenzelm |
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
|
file |
diff |
annotate
|
| Wed, 15 Apr 2015 21:20:37 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 14 Apr 2015 22:54:07 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 00:26:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 22:18:33 +0100 |
paulson |
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 12:47:46 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 12:40:03 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 23:56:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 12:16:45 +0200 |
nipkow |
renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 20:42:38 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 20:42:32 +0200 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 18:00:58 +0200 |
blanchet |
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:24:32 +0200 |
blanchet |
tuned wording
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:15:55 +0200 |
blanchet |
Z3 news
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 15:21:20 +0200 |
blanchet |
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 11:13:53 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Tue, 07 Apr 2015 18:21:56 +0200 |
nipkow |
Removed mcard because it is equal to size
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 22:01:30 +0200 |
wenzelm |
some explanation of 'private';
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 22:40:41 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 22:08:06 +0200 |
wenzelm |
added command 'experiment';
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 19:31:28 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 16:24:38 +0200 |
wenzelm |
added isabelle build option -x, to exclude sessions;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 15:41:08 +0200 |
wenzelm |
added isabelle build option -k, for fast off-line checking of theory sources;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 14:48:38 +0100 |
paulson |
HOL Light Libraries for complex Arctan, Arcsin, Arccos
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 00:13:37 +0200 |
wenzelm |
clarified NEWS (cf. 97872c658a44);
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 16:22:35 +0200 |
wenzelm |
rule_insts_schematic is considered legacy and false by default;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:05:14 +0100 |
haftmann |
explicit commutative additive inverse operation;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 17:51:34 +0100 |
blanchet |
more multiset theorems
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 10:59:28 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 15:57:51 +0100 |
wenzelm |
admit dummy patterns in instantiations;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 23:16:40 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2015 14:24:51 +0000 |
paulson |
New material for complex sin, cos, tan, Ln, also some reorganisation
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 17:23:22 +0000 |
paulson |
new HOL Light material about exp, sin, cos
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 13:51:33 +0100 |
noschinl |
added proof method rewrite
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 12:23:56 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 15:30:00 +0000 |
paulson |
The factorial function, "fact", now has type "nat => 'a"
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 23:04:40 +0100 |
blanchet |
documented renamed theories
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 21:30:42 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 20:33:33 +0100 |
wenzelm |
support structural composition (THEN_ALL_NEW) for proof methods;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 16:42:18 +0000 |
paulson |
Removed the infix operator "choose" to allow HOLCF to build
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 22:38:11 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 23:31:13 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 23:31:04 +0100 |
nipkow |
Removed the obsolete functions "natfloor" and "natceiling"
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2015 08:50:00 +0100 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Fri, 27 Feb 2015 15:41:28 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 23 Feb 2015 14:50:30 +0100 |
wenzelm |
Goal.prove_multi is superseded by the fully general Goal.prove_common;
|
file |
diff |
annotate
|
| Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
| Wed, 18 Feb 2015 22:46:48 +0100 |
haftmann |
eliminated fact duplicates
|
file |
diff |
annotate
|