| Fri, 30 Dec 2011 16:43:46 +0100 |
wenzelm |
eliminated old-fashioned Global_Theory.add_thms;
|
changeset |
files
|
| Fri, 30 Dec 2011 15:43:07 +0100 |
wenzelm |
simplified proof -- avoid res_inst_tac, afford plain asm_full_simp_tac;
|
changeset |
files
|
| Fri, 30 Dec 2011 14:19:58 +0100 |
wenzelm |
simplified proof;
|
changeset |
files
|
| Fri, 30 Dec 2011 13:52:07 +0100 |
wenzelm |
simplified proof;
|
changeset |
files
|
| Fri, 30 Dec 2011 12:54:55 +0100 |
wenzelm |
simplified proof;
|
changeset |
files
|
| Fri, 30 Dec 2011 12:12:16 +0100 |
wenzelm |
more parallelism;
|
changeset |
files
|
| Fri, 30 Dec 2011 12:00:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 29 Dec 2011 20:32:59 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 29 Dec 2011 20:31:58 +0100 |
wenzelm |
tuned -- afford slightly larger simpset in simp_defs_tac;
|
changeset |
files
|
| Thu, 29 Dec 2011 20:05:53 +0100 |
wenzelm |
tuned -- standard proofs by default;
|
changeset |
files
|
| Thu, 29 Dec 2011 19:37:24 +0100 |
wenzelm |
do not fork skipped proofs;
|
changeset |
files
|
| Thu, 29 Dec 2011 18:27:17 +0100 |
wenzelm |
clarified timeit_msg;
|
changeset |
files
|
| Thu, 29 Dec 2011 16:58:19 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 29 Dec 2011 15:54:37 +0100 |
wenzelm |
comments;
|
changeset |
files
|
| Thu, 29 Dec 2011 18:54:07 +0100 |
huffman |
remove constant 'ccpo.lub', re-use constant 'Sup' instead
|
changeset |
files
|
| Thu, 29 Dec 2011 17:43:54 +0100 |
nipkow |
merged
|
changeset |
files
|
| Thu, 29 Dec 2011 17:43:40 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 29 Dec 2011 15:14:44 +0100 |
haftmann |
conversions from sets to predicates and vice versa; extensionality on predicates
|
changeset |
files
|
| Thu, 29 Dec 2011 15:14:44 +0100 |
haftmann |
added implementation of pred_of_set
|
changeset |
files
|
| Thu, 29 Dec 2011 14:23:40 +0100 |
haftmann |
fundamental theorems on Set.bind
|
changeset |
files
|
| Thu, 29 Dec 2011 14:44:44 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Thu, 29 Dec 2011 13:42:21 +0100 |
haftmann |
qualified Finite_Set.fold
|
changeset |
files
|
| Thu, 29 Dec 2011 13:41:41 +0100 |
haftmann |
qualified Finite_Set.fold
|
changeset |
files
|
| Thu, 29 Dec 2011 10:47:56 +0100 |
haftmann |
dropped redundant setup
|
changeset |
files
|
| Thu, 29 Dec 2011 10:47:56 +0100 |
haftmann |
tuned declaration
|
changeset |
files
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post; tuned text
|
changeset |
files
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post; tuned names and spacing
|
changeset |
files
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
changeset |
files
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post
|
changeset |
files
|
| Thu, 29 Dec 2011 10:47:54 +0100 |
haftmann |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
|
changeset |
files
|