| Mon, 23 Aug 2010 19:35:57 +0200 |
Rewrite the Probability theory.
|
file | diff | annotate |
| Mon, 23 Aug 2010 11:17:13 +0200 |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file | diff | annotate |
| Fri, 20 Aug 2010 17:48:30 +0200 |
split and enriched theory SetsAndFunctions
|
file | diff | annotate |
| Thu, 19 Aug 2010 17:41:52 +0200 |
merged
|
file | diff | annotate |
| Tue, 17 Aug 2010 18:41:55 +0200 |
discontinued support for Poly/ML 5.0 and 5.1 versions;
|
file | diff | annotate |
| Thu, 19 Aug 2010 16:08:53 +0200 |
deglobalized named HOL constants
|
file | diff | annotate |
| Wed, 18 Aug 2010 17:03:09 +0200 |
merged
|
file | diff | annotate |
| Wed, 18 Aug 2010 17:01:12 +0200 |
NEWS
|
file | diff | annotate |
| Wed, 18 Aug 2010 15:01:57 +0200 |
more helpful NEWS entry
|
file | diff | annotate |
| Tue, 17 Aug 2010 16:44:21 +0200 |
preemptive NEWS
|
file | diff | annotate |
| Wed, 18 Aug 2010 14:55:09 +0200 |
NEWS
|
file | diff | annotate |
| Wed, 18 Aug 2010 12:26:48 +0200 |
deglobalization
|
file | diff | annotate |
| Tue, 17 Aug 2010 14:33:39 +0200 |
NEWS and CONTRIBUTORS
|
file | diff | annotate |
| Wed, 11 Aug 2010 14:31:40 +0200 |
NEWS
|
file | diff | annotate |
| Tue, 03 Aug 2010 16:33:11 +0200 |
theory loading: only the master source file is looked-up in the implicit load path;
|
file | diff | annotate |
| Sat, 31 Jul 2010 23:32:05 +0200 |
Documentation of 'interpret' updated.
|
file | diff | annotate |
| Thu, 22 Jul 2010 22:31:20 +0200 |
discontinued special treatment of ML files -- no longer complete extensions on demand;
|
file | diff | annotate |
| Wed, 21 Jul 2010 15:02:51 +0200 |
ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
|
file | diff | annotate |
| Wed, 14 Jul 2010 14:53:44 +0200 |
export_code without file prints to standard output
|
file | diff | annotate |
| Wed, 07 Jul 2010 08:25:22 +0200 |
added NEWS entry
|
file | diff | annotate |
| Fri, 02 Jul 2010 10:47:50 +0200 |
fixed spelling
|
file | diff | annotate |
| Thu, 01 Jul 2010 16:55:05 +0200 |
"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
|
file | diff | annotate |
| Thu, 01 Jul 2010 10:57:19 +0200 |
Updated NEWS
|
file | diff | annotate |
| Tue, 29 Jun 2010 07:55:18 +0200 |
merged
|
file | diff | annotate |
| Mon, 28 Jun 2010 15:32:06 +0200 |
dropped ancient infix mem; refined code generation operations in List.thy
|
file | diff | annotate |
| Mon, 28 Jun 2010 15:03:07 +0200 |
merged constants "split" and "prod_case"
|
file | diff | annotate |
| Fri, 25 Jun 2010 11:48:37 +0200 |
explicit treatment of UTF8 sequences as Isabelle symbols;
|
file | diff | annotate |
| Mon, 21 Jun 2010 17:41:57 +0200 |
merged, resolving conflicts in doc-src/IsarRef/Thy/HOL_Specific.thy;
|
file | diff | annotate |
| Mon, 21 Jun 2010 11:24:19 +0200 |
final tuning;
|
file | diff | annotate |
| Fri, 11 Jun 2010 13:25:28 +0200 |
NEWS: IsabelleText font;
|
file | diff | annotate |
| Mon, 07 Jun 2010 17:52:30 +0200 |
Documented changes in induct, cases, and nominal_induct method.
|
file | diff | annotate |
| Tue, 15 Jun 2010 14:28:22 +0200 |
added code_simp infrastructure
|
file | diff | annotate |
| Tue, 15 Jun 2010 07:42:48 +0200 |
merged
|
file | diff | annotate |
| Mon, 14 Jun 2010 12:01:30 +0200 |
NEWS
|
file | diff | annotate |
| Mon, 14 Jun 2010 15:10:36 +0200 |
removed simplifier congruence rule of "prod_case"
|
file | diff | annotate |
| Thu, 10 Jun 2010 12:24:01 +0200 |
qualified type "*"; qualified constants Pair, fst, snd, split
|
file | diff | annotate |
| Tue, 08 Jun 2010 16:37:19 +0200 |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
file | diff | annotate |
| Mon, 07 Jun 2010 17:39:32 +0200 |
back to non-release mode;
|
file | diff | annotate |
| Mon, 07 Jun 2010 11:42:32 +0200 |
more NEWS;
|
file | diff | annotate |
| Mon, 07 Jun 2010 11:27:08 +0200 |
more NEWS;
|
file | diff | annotate |
| Fri, 04 Jun 2010 16:02:46 +0200 |
NEWS (more strict internal axioms/defs format)
|
file | diff | annotate |
| Fri, 04 Jun 2010 11:30:46 +0200 |
spelling;
|
file | diff | annotate |
| Thu, 03 Jun 2010 22:17:36 +0200 |
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
|
file | diff | annotate |
| Thu, 03 Jun 2010 16:39:50 +0200 |
clarified
|
file | diff | annotate |
| Thu, 03 Jun 2010 16:39:05 +0200 |
mention unconstrain in NEWS
|
file | diff | annotate |
| Wed, 02 Jun 2010 21:53:03 +0200 |
improved parallelism of proof term normalization;
|
file | diff | annotate |
| Tue, 01 Jun 2010 17:52:19 +0200 |
merged
|
file | diff | annotate |
| Tue, 01 Jun 2010 17:52:00 +0200 |
update NEWS
|
file | diff | annotate |
| Tue, 01 Jun 2010 15:38:47 +0200 |
removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
|
file | diff | annotate |
| Tue, 01 Jun 2010 12:20:08 +0200 |
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
|
file | diff | annotate |
| Mon, 31 May 2010 22:08:40 +0200 |
notes on Isabelle/jEdit;
|
file | diff | annotate |
| Mon, 31 May 2010 21:06:57 +0200 |
modernized some structure names, keeping a few legacy aliases;
|
file | diff | annotate |
| Thu, 27 May 2010 21:37:42 +0200 |
merged
|
file | diff | annotate |
| Thu, 27 May 2010 18:10:37 +0200 |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file | diff | annotate |
| Thu, 27 May 2010 17:41:27 +0200 |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file | diff | annotate |
| Thu, 27 May 2010 16:30:26 +0200 |
merged
|
file | diff | annotate |
| Thu, 27 May 2010 14:54:13 +0200 |
moved SMT into the HOL image
|
file | diff | annotate |
| Thu, 27 May 2010 15:28:23 +0200 |
misc updates for release;
|
file | diff | annotate |
| Thu, 27 May 2010 15:15:20 +0200 |
constant Rat.normalize needs to be qualified;
|
file | diff | annotate |
| Sat, 22 May 2010 17:44:12 -0700 |
NEWS: removed fixrec_simp attribute
|
file | diff | annotate |