wenzelm [Sat, 10 Sep 2011 20:39:13 +0200] rev 44867
stronger colors (as background);
wenzelm [Sat, 10 Sep 2011 20:22:22 +0200] rev 44866
some color scheme for theory status;
wenzelm [Sat, 10 Sep 2011 16:30:08 +0200] rev 44865
some keyboard shortcuts for important actions;
proper label properties, which are also required for jEdit "Shortcuts" options panel;
wenzelm [Sat, 10 Sep 2011 14:48:06 +0200] rev 44864
explicit jEdit actions -- to enable key mappings, for example;
wenzelm [Sat, 10 Sep 2011 14:28:07 +0200] rev 44863
more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm [Sat, 10 Sep 2011 13:43:09 +0200] rev 44862
tuned usage;
wenzelm [Sat, 10 Sep 2011 13:41:03 +0200] rev 44861
simplified default Isabelle application wrapper (NB: build process is already part of isabelle jedit tool);
haftmann [Sat, 10 Sep 2011 10:29:24 +0200] rev 44860
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
blanchet [Sat, 10 Sep 2011 00:44:25 +0200] rev 44859
fixed definition of type intersection (soundness bug)
blanchet [Sat, 10 Sep 2011 00:44:25 +0200] rev 44858
continue with minimization in debug mode in spite of unsoundness
huffman [Fri, 09 Sep 2011 09:31:04 -0700] rev 44857
generalize lemma of_nat_number_of_eq to class number_semiring
bulwahn [Fri, 09 Sep 2011 15:14:59 +0200] rev 44856
merged
bulwahn [Fri, 09 Sep 2011 14:43:50 +0200] rev 44855
stating more explicitly our expectation that these two terms have the same term structure
bulwahn [Fri, 09 Sep 2011 12:33:09 +0200] rev 44854
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
blanchet [Fri, 09 Sep 2011 14:30:57 +0200] rev 44853
made SML/NJ happy
noschinl [Thu, 08 Sep 2011 12:23:11 +0200] rev 44852
call ghc with -XEmptyDataDecls
nipkow [Fri, 09 Sep 2011 06:47:14 +0200] rev 44851
merged
nipkow [Fri, 09 Sep 2011 06:45:39 +0200] rev 44850
tuned headers
huffman [Thu, 08 Sep 2011 19:35:23 -0700] rev 44849
Library/Saturated.thy: number_semiring class instance
huffman [Thu, 08 Sep 2011 18:47:23 -0700] rev 44848
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman [Thu, 08 Sep 2011 18:13:48 -0700] rev 44847
merged
huffman [Thu, 08 Sep 2011 10:07:53 -0700] rev 44846
remove unnecessary intermediate lemmas
krauss [Fri, 09 Sep 2011 00:22:18 +0200] rev 44845
added syntactic classes for "inf" and "sup"
huffman [Thu, 08 Sep 2011 08:41:28 -0700] rev 44844
prove existence, uniqueness, and other properties of complex arg function
huffman [Thu, 08 Sep 2011 07:27:57 -0700] rev 44843
tuned
huffman [Thu, 08 Sep 2011 07:16:47 -0700] rev 44842
remove obsolete intermediate lemma complex_inverse_complex_split
huffman [Thu, 08 Sep 2011 07:06:59 -0700] rev 44841
tuned
haftmann [Thu, 08 Sep 2011 11:31:53 +0200] rev 44840
merged
haftmann [Thu, 08 Sep 2011 11:31:23 +0200] rev 44839
tuned
haftmann [Thu, 08 Sep 2011 00:35:22 +0200] rev 44838
merged
haftmann [Wed, 07 Sep 2011 08:13:38 +0200] rev 44837
merged
haftmann [Tue, 06 Sep 2011 22:37:32 +0200] rev 44836
merged
haftmann [Tue, 06 Sep 2011 22:04:14 +0200] rev 44835
merged
haftmann [Tue, 06 Sep 2011 07:23:45 +0200] rev 44834
merged
haftmann [Mon, 05 Sep 2011 22:02:32 +0200] rev 44833
tuned
haftmann [Mon, 05 Sep 2011 19:18:38 +0200] rev 44832
merged
haftmann [Mon, 05 Sep 2011 07:49:31 +0200] rev 44831
tuned
haftmann [Sun, 04 Sep 2011 09:28:15 +0200] rev 44830
tuned
blanchet [Thu, 08 Sep 2011 09:25:55 +0200] rev 44829
fixed computation of "in_conj" for polymorphic encodings
huffman [Wed, 07 Sep 2011 22:44:26 -0700] rev 44828
add some new lemmas about cis and rcis;
simplify some proofs;
huffman [Wed, 07 Sep 2011 20:44:39 -0700] rev 44827
Complex.thy: move theorems into appropriate subsections
huffman [Wed, 07 Sep 2011 19:24:28 -0700] rev 44826
merged
huffman [Wed, 07 Sep 2011 17:41:29 -0700] rev 44825
remove redundant lemma complex_of_real_minus_one
huffman [Wed, 07 Sep 2011 18:47:55 -0700] rev 44824
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
huffman [Wed, 07 Sep 2011 10:04:07 -0700] rev 44823
removed unused lemma sin_cos_squared_add2_mult
huffman [Wed, 07 Sep 2011 09:45:39 -0700] rev 44822
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
huffman [Wed, 07 Sep 2011 09:02:58 -0700] rev 44821
avoid using legacy theorem names
wenzelm [Thu, 08 Sep 2011 00:23:23 +0200] rev 44820
merged
haftmann [Wed, 07 Sep 2011 23:55:40 +0200] rev 44819
theory of saturated naturals contributed by Peter Gammie
haftmann [Wed, 07 Sep 2011 23:38:52 +0200] rev 44818
theory of saturated naturals contributed by Peter Gammie
haftmann [Wed, 07 Sep 2011 23:07:16 +0200] rev 44817
lemmas about +, *, min, max on nat
blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44816
update Sledgehammer docs
blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44815
added new tagged encodings to Metis tests
blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44814
also implemented ghost version of the tagged encodings
blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44813
added new guards encoding to test
blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44812
smarter explicit apply business
blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44811
started work on ghost type arg encoding
blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44810
stricted type encoding parsing
wenzelm [Thu, 08 Sep 2011 00:20:09 +0200] rev 44809
more substructural sharing to gain significant compression;
wenzelm [Wed, 07 Sep 2011 23:08:04 +0200] rev 44808
XML.cache for partial sharing (strings only);