| Sat, 17 Sep 2011 17:05:31 +0200 |
wenzelm |
removed obsolete patches for PG 4.1;
|
changeset |
files
|
| Sat, 17 Sep 2011 16:53:01 +0200 |
wenzelm |
specific bundle for x86_64-linux, which is especially important for JRE due to its extra library dependencies;
|
changeset |
files
|
| Sat, 17 Sep 2011 16:29:18 +0200 |
wenzelm |
added "isabelle scalac" convenience;
|
changeset |
files
|
| Sat, 17 Sep 2011 16:19:40 +0200 |
wenzelm |
Symbol.explode as in ML;
|
changeset |
files
|
| Sat, 17 Sep 2011 16:00:54 +0200 |
wenzelm |
ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;
|
changeset |
files
|
| Sat, 17 Sep 2011 15:08:55 +0200 |
haftmann |
dropped unused argument – avoids problem with SML/NJ
|
changeset |
files
|
| Sat, 17 Sep 2011 00:40:27 +0200 |
haftmann |
tuned spacing
|
changeset |
files
|
| Sat, 17 Sep 2011 00:37:21 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sat, 17 Sep 2011 04:41:44 +0200 |
nipkow |
tuned post fixpoint setup
|
changeset |
files
|
| Sat, 17 Sep 2011 03:37:14 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 16 Sep 2011 09:18:15 +0200 |
nipkow |
when applying induction rules, remove names of assumptions that come
|
changeset |
files
|
| Fri, 16 Sep 2011 20:08:29 +0200 |
noschinl |
remove stray "using [[simp_trace]]"
|
changeset |
files
|
| Fri, 16 Sep 2011 20:02:35 +0200 |
noschinl |
tune indenting
|
changeset |
files
|
| Fri, 16 Sep 2011 12:10:43 +1000 |
kleing |
removed unused legacy lemma names, some comment cleanup.
|
changeset |
files
|
| Fri, 16 Sep 2011 12:10:15 +1000 |
kleing |
removed word_neq_0_conv from simpset, it's almost never wanted.
|
changeset |
files
|
| Thu, 15 Sep 2011 12:40:08 -0400 |
hoelzl |
removed further legacy rules from Complete_Lattices
|
changeset |
files
|
| Thu, 15 Sep 2011 17:06:00 +0200 |
noschinl |
NEWS on Complete_Lattices, Lattices
|
changeset |
files
|
| Thu, 15 Sep 2011 10:57:40 +0200 |
blanchet |
tail recursive proof preprocessing (needed for huge proofs)
|
changeset |
files
|
| Thu, 15 Sep 2011 10:57:40 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 15 Sep 2011 09:44:27 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 15 Sep 2011 09:44:08 +0200 |
nipkow |
revised AbsInt and added widening and narrowing
|
changeset |
files
|
| Wed, 14 Sep 2011 23:47:04 +0200 |
haftmann |
updated comment
|
changeset |
files
|
| Wed, 14 Sep 2011 23:46:02 +0200 |
haftmann |
updated generated code
|
changeset |
files
|
| Tue, 13 Sep 2011 07:56:46 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
changeset |
files
|
| Wed, 14 Sep 2011 10:55:07 +0200 |
noschinl |
merged
|
changeset |
files
|
| Wed, 14 Sep 2011 10:24:22 +0200 |
noschinl |
create central list for language extensions used by the haskell code generator
|
changeset |
files
|
| Wed, 14 Sep 2011 09:46:59 +0200 |
boehmes |
observe distinction between sets and predicates
|
changeset |
files
|
| Wed, 14 Sep 2011 06:49:24 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 14 Sep 2011 06:49:01 +0200 |
nipkow |
cleand up AbsInt fixpoint iteration; tuned syntax
|
changeset |
files
|
| Tue, 13 Sep 2011 17:25:19 -0700 |
huffman |
tuned proofs
|
changeset |
files
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
changeset |
files
|
| Tue, 13 Sep 2011 08:21:51 -0700 |
huffman |
remove some redundant [simp] declarations;
|
changeset |
files
|
| Tue, 13 Sep 2011 16:22:01 +0200 |
noschinl |
tune proofs
|
changeset |
files
|
| Tue, 13 Sep 2011 16:21:48 +0200 |
noschinl |
tune simpset for Complete_Lattices
|
changeset |
files
|
| Tue, 13 Sep 2011 13:17:52 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 13 Sep 2011 12:14:29 +0200 |
bulwahn |
added lemma motivated by a more specific lemma in the AFP-KBPs theories
|
changeset |
files
|
| Tue, 13 Sep 2011 11:24:58 +0200 |
blanchet |
simplified unsound proof detection by removing impossible case
|
changeset |
files
|
| Tue, 13 Sep 2011 09:56:38 +0200 |
bulwahn |
correcting NEWS
|
changeset |
files
|
| Tue, 13 Sep 2011 09:28:03 +0200 |
bulwahn |
correcting theory name and dependencies
|
changeset |
files
|
| Tue, 13 Sep 2011 09:25:19 +0200 |
bulwahn |
renamed AList_Impl to AList
|
changeset |
files
|
| Tue, 13 Sep 2011 07:13:49 +0200 |
nipkow |
fastsimp -> fastforce in doc
|
changeset |
files
|
| Mon, 12 Sep 2011 14:49:34 -0700 |
huffman |
fix typo
|
changeset |
files
|
| Mon, 12 Sep 2011 14:39:10 -0700 |
huffman |
shorten proof of frontier_straddle
|
changeset |
files
|
| Mon, 12 Sep 2011 13:19:10 -0700 |
huffman |
NEWS and CONTRIBUTORS
|
changeset |
files
|
| Mon, 12 Sep 2011 11:54:20 -0700 |
huffman |
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
|
changeset |
files
|
| Mon, 12 Sep 2011 11:39:29 -0700 |
huffman |
simplify proofs using LIMSEQ lemmas
|
changeset |
files
|
| Mon, 12 Sep 2011 10:43:36 -0700 |
huffman |
remove trivial lemma Lim_at_iff_LIM
|
changeset |
files
|
| Mon, 12 Sep 2011 10:28:45 -0700 |
huffman |
fix typos
|
changeset |
files
|
| Mon, 12 Sep 2011 09:37:49 -0700 |
huffman |
NEWS for euclidean_space class
|
changeset |
files
|
| Mon, 12 Sep 2011 09:21:01 -0700 |
huffman |
move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
|
changeset |
files
|
| Mon, 12 Sep 2011 09:57:33 -0400 |
hoelzl |
adding NEWS and CONTRIBUTORS
|
changeset |
files
|
| Mon, 12 Sep 2011 13:35:35 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Mon, 12 Sep 2011 12:33:37 +0200 |
bulwahn |
correcting imports after splitting and renaming AssocList
|
changeset |
files
|
| Mon, 12 Sep 2011 10:59:38 +0200 |
bulwahn |
tuned
|
changeset |
files
|
| Mon, 12 Sep 2011 10:57:58 +0200 |
bulwahn |
moving connection of association lists to Mappings into a separate theory
|
changeset |
files
|
| Mon, 12 Sep 2011 10:27:36 +0200 |
bulwahn |
adding NEWS and CONTRIBUTORS
|
changeset |
files
|
| Mon, 12 Sep 2011 09:45:53 +0200 |
bulwahn |
tuned some symbol that probably went there by some strange encoding issue
|
changeset |
files
|
| Mon, 12 Sep 2011 11:05:32 +0200 |
blanchet |
added my contributions to NEWS and CONTRIBUTORS
|
changeset |
files
|
| Mon, 12 Sep 2011 10:49:37 +0200 |
blanchet |
fixed type intersection (again)
|
changeset |
files
|
| Mon, 12 Sep 2011 10:49:37 +0200 |
blanchet |
consistent option naming
|
changeset |
files
|
| Mon, 12 Sep 2011 09:07:23 +0200 |
nipkow |
NEWS fastsimp -> fastforce
|
changeset |
files
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
changeset |
files
|
| Sun, 11 Sep 2011 22:56:05 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 11 Sep 2011 13:49:42 -0700 |
huffman |
NEWS for Library/Product_Lattice.thy
|
changeset |
files
|
| Sun, 11 Sep 2011 22:55:26 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sun, 11 Sep 2011 21:35:35 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 11 Sep 2011 10:30:50 -0700 |
huffman |
merged
|
changeset |
files
|
| Sun, 11 Sep 2011 09:40:18 -0700 |
huffman |
tuned proofs
|
changeset |
files
|
| Sun, 11 Sep 2011 07:21:45 -0700 |
huffman |
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
|
changeset |
files
|
| Sun, 11 Sep 2011 21:34:23 +0200 |
wenzelm |
more CONTRIBUTORS;
|
changeset |
files
|
| Sun, 11 Sep 2011 20:19:20 +0200 |
wenzelm |
persistent ISABELLE_INTERFACE_CHOICE;
|
changeset |
files
|
| Sun, 11 Sep 2011 19:52:09 +0200 |
wenzelm |
explicit choice of interface;
|
changeset |
files
|
| Sun, 11 Sep 2011 17:30:01 +0200 |
wenzelm |
more orthogonal signature;
|
changeset |
files
|
| Sun, 11 Sep 2011 15:20:09 +0200 |
wenzelm |
updates for release;
|
changeset |
files
|
| Sun, 11 Sep 2011 14:58:52 +0200 |
wenzelm |
misc tuning and clarification (NB: settings are already local for named snapshots/releases);
|
changeset |
files
|
| Sun, 11 Sep 2011 14:42:15 +0200 |
wenzelm |
some updates of PLATFORMS;
|
changeset |
files
|
| Sun, 11 Sep 2011 13:27:22 +0200 |
wenzelm |
more README;
|
changeset |
files
|
| Sat, 10 Sep 2011 23:28:58 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 10 Sep 2011 22:43:17 +0200 |
krauss |
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
|
changeset |
files
|
| Sat, 10 Sep 2011 23:27:32 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 10 Sep 2011 22:11:55 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sat, 10 Sep 2011 21:47:55 +0200 |
wenzelm |
speed up slow proof;
|
changeset |
files
|
| Sat, 10 Sep 2011 20:41:27 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 10 Sep 2011 19:44:41 +0200 |
haftmann |
more modularization
|
changeset |
files
|
| Sat, 10 Sep 2011 20:39:13 +0200 |
wenzelm |
stronger colors (as background);
|
changeset |
files
|
| Sat, 10 Sep 2011 20:22:22 +0200 |
wenzelm |
some color scheme for theory status;
|
changeset |
files
|
| Sat, 10 Sep 2011 16:30:08 +0200 |
wenzelm |
some keyboard shortcuts for important actions;
|
changeset |
files
|
| Sat, 10 Sep 2011 14:48:06 +0200 |
wenzelm |
explicit jEdit actions -- to enable key mappings, for example;
|
changeset |
files
|
| Sat, 10 Sep 2011 14:28:07 +0200 |
wenzelm |
more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
|
changeset |
files
|
| Sat, 10 Sep 2011 13:43:09 +0200 |
wenzelm |
tuned usage;
|
changeset |
files
|
| Sat, 10 Sep 2011 13:41:03 +0200 |
wenzelm |
simplified default Isabelle application wrapper (NB: build process is already part of isabelle jedit tool);
|
changeset |
files
|
| Sat, 10 Sep 2011 10:29:24 +0200 |
haftmann |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
|
changeset |
files
|
| Sat, 10 Sep 2011 00:44:25 +0200 |
blanchet |
fixed definition of type intersection (soundness bug)
|
changeset |
files
|
| Sat, 10 Sep 2011 00:44:25 +0200 |
blanchet |
continue with minimization in debug mode in spite of unsoundness
|
changeset |
files
|
| Fri, 09 Sep 2011 09:31:04 -0700 |
huffman |
generalize lemma of_nat_number_of_eq to class number_semiring
|
changeset |
files
|
| Fri, 09 Sep 2011 15:14:59 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Fri, 09 Sep 2011 14:43:50 +0200 |
bulwahn |
stating more explicitly our expectation that these two terms have the same term structure
|
changeset |
files
|
| Fri, 09 Sep 2011 12:33:09 +0200 |
bulwahn |
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
|
changeset |
files
|
| Fri, 09 Sep 2011 14:30:57 +0200 |
blanchet |
made SML/NJ happy
|
changeset |
files
|
| Thu, 08 Sep 2011 12:23:11 +0200 |
noschinl |
call ghc with -XEmptyDataDecls
|
changeset |
files
|
| Fri, 09 Sep 2011 06:47:14 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 09 Sep 2011 06:45:39 +0200 |
nipkow |
tuned headers
|
changeset |
files
|
| Thu, 08 Sep 2011 19:35:23 -0700 |
huffman |
Library/Saturated.thy: number_semiring class instance
|
changeset |
files
|
| Thu, 08 Sep 2011 18:47:23 -0700 |
huffman |
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
|
changeset |
files
|
| Thu, 08 Sep 2011 18:13:48 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 08 Sep 2011 10:07:53 -0700 |
huffman |
remove unnecessary intermediate lemmas
|
changeset |
files
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
changeset |
files
|
| Thu, 08 Sep 2011 08:41:28 -0700 |
huffman |
prove existence, uniqueness, and other properties of complex arg function
|
changeset |
files
|
| Thu, 08 Sep 2011 07:27:57 -0700 |
huffman |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 07:16:47 -0700 |
huffman |
remove obsolete intermediate lemma complex_inverse_complex_split
|
changeset |
files
|
| Thu, 08 Sep 2011 07:06:59 -0700 |
huffman |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 11:31:53 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 08 Sep 2011 11:31:23 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 00:35:22 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 08:13:38 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 22:37:32 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 22:04:14 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 07:23:45 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 05 Sep 2011 22:02:32 +0200 |
haftmann |
tuned
|
changeset |
files
|