| 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
|
| Mon, 05 Sep 2011 19:18:38 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 05 Sep 2011 07:49:31 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sun, 04 Sep 2011 09:28:15 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 09:25:55 +0200 |
blanchet |
fixed computation of "in_conj" for polymorphic encodings
|
changeset |
files
|
| Wed, 07 Sep 2011 22:44:26 -0700 |
huffman |
add some new lemmas about cis and rcis;
|
changeset |
files
|
| Wed, 07 Sep 2011 20:44:39 -0700 |
huffman |
Complex.thy: move theorems into appropriate subsections
|
changeset |
files
|
| Wed, 07 Sep 2011 19:24:28 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 17:41:29 -0700 |
huffman |
remove redundant lemma complex_of_real_minus_one
|
changeset |
files
|
| Wed, 07 Sep 2011 18:47:55 -0700 |
huffman |
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
|
changeset |
files
|
| Wed, 07 Sep 2011 10:04:07 -0700 |
huffman |
removed unused lemma sin_cos_squared_add2_mult
|
changeset |
files
|
| Wed, 07 Sep 2011 09:45:39 -0700 |
huffman |
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
|
changeset |
files
|
| Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
changeset |
files
|
| Thu, 08 Sep 2011 00:23:23 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 23:55:40 +0200 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
changeset |
files
|
| Wed, 07 Sep 2011 23:38:52 +0200 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
changeset |
files
|
| Wed, 07 Sep 2011 23:07:16 +0200 |
haftmann |
lemmas about +, *, min, max on nat
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
update Sledgehammer docs
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
added new tagged encodings to Metis tests
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
also implemented ghost version of the tagged encodings
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
added new guards encoding to test
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
smarter explicit apply business
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
started work on ghost type arg encoding
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
stricted type encoding parsing
|
changeset |
files
|
| Thu, 08 Sep 2011 00:20:09 +0200 |
wenzelm |
more substructural sharing to gain significant compression;
|
changeset |
files
|
| Wed, 07 Sep 2011 23:08:04 +0200 |
wenzelm |
XML.cache for partial sharing (strings only);
|
changeset |
files
|
| Wed, 07 Sep 2011 22:00:41 +0200 |
wenzelm |
platform-specific look and feel;
|
changeset |
files
|
| Wed, 07 Sep 2011 21:41:36 +0200 |
wenzelm |
more README;
|
changeset |
files
|
| Wed, 07 Sep 2011 21:38:48 +0200 |
wenzelm |
clarified terminology;
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:50 +0200 |
wenzelm |
no print_state for final proof commands, which return to theory state;
|
changeset |
files
|
| Wed, 07 Sep 2011 21:10:47 +0200 |
wenzelm |
NEWS on IsabelleText font;
|
changeset |
files
|
| Wed, 07 Sep 2011 21:05:53 +0200 |
wenzelm |
explicit join_syntax ensures command transaction integrity of 'theory';
|
changeset |
files
|
| Wed, 07 Sep 2011 20:49:45 +0200 |
wenzelm |
some updates for release;
|
changeset |
files
|
| Wed, 07 Sep 2011 20:29:54 +0200 |
wenzelm |
some tuning for release;
|
changeset |
files
|
| Wed, 07 Sep 2011 18:01:01 +0200 |
wenzelm |
updated file locations;
|
changeset |
files
|
| Wed, 07 Sep 2011 17:42:57 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 14:58:40 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:39 +0200 |
bulwahn |
removing previously used function locally_monomorphic in the code generator
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:38 +0200 |
bulwahn |
setting const_sorts to false in the type inference of the code generator
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:37 +0200 |
bulwahn |
adapting Imperative HOL serializer to changes of the iterm datatype in the code generator
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:36 +0200 |
bulwahn |
removing previous crude approximation to add type annotations to disambiguate types
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:35 +0200 |
bulwahn |
adding minimalistic implementation for printing the type annotations
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:34 +0200 |
bulwahn |
adding call to disambiguation annotations
|
changeset |
files
|