huffman [Mon, 12 Sep 2011 10:28:45 -0700] rev 44904
fix typos
huffman [Mon, 12 Sep 2011 09:37:49 -0700] rev 44903
NEWS for euclidean_space class
huffman [Mon, 12 Sep 2011 09:21:01 -0700] rev 44902
move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
hoelzl [Mon, 12 Sep 2011 09:57:33 -0400] rev 44901
adding NEWS and CONTRIBUTORS
bulwahn [Mon, 12 Sep 2011 13:35:35 +0200] rev 44900
merged
bulwahn [Mon, 12 Sep 2011 12:33:37 +0200] rev 44899
correcting imports after splitting and renaming AssocList
bulwahn [Mon, 12 Sep 2011 10:59:38 +0200] rev 44898
tuned
bulwahn [Mon, 12 Sep 2011 10:57:58 +0200] rev 44897
moving connection of association lists to Mappings into a separate theory
bulwahn [Mon, 12 Sep 2011 10:27:36 +0200] rev 44896
adding NEWS and CONTRIBUTORS
bulwahn [Mon, 12 Sep 2011 09:45:53 +0200] rev 44895
tuned some symbol that probably went there by some strange encoding issue
blanchet [Mon, 12 Sep 2011 11:05:32 +0200] rev 44894
added my contributions to NEWS and CONTRIBUTORS
blanchet [Mon, 12 Sep 2011 10:49:37 +0200] rev 44893
fixed type intersection (again)
blanchet [Mon, 12 Sep 2011 10:49:37 +0200] rev 44892
consistent option naming
nipkow [Mon, 12 Sep 2011 09:07:23 +0200] rev 44891
NEWS fastsimp -> fastforce
nipkow [Mon, 12 Sep 2011 07:55:43 +0200] rev 44890
new fastforce replacing fastsimp - less confusing name
wenzelm [Sun, 11 Sep 2011 22:56:05 +0200] rev 44889
merged
huffman [Sun, 11 Sep 2011 13:49:42 -0700] rev 44888
NEWS for Library/Product_Lattice.thy
wenzelm [Sun, 11 Sep 2011 22:55:26 +0200] rev 44887
misc tuning and clarification;
wenzelm [Sun, 11 Sep 2011 21:35:35 +0200] rev 44886
merged
huffman [Sun, 11 Sep 2011 10:30:50 -0700] rev 44885
merged
huffman [Sun, 11 Sep 2011 09:40:18 -0700] rev 44884
tuned proofs
huffman [Sun, 11 Sep 2011 07:21:45 -0700] rev 44883
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
wenzelm [Sun, 11 Sep 2011 21:34:23 +0200] rev 44882
more CONTRIBUTORS;
wenzelm [Sun, 11 Sep 2011 20:19:20 +0200] rev 44881
persistent ISABELLE_INTERFACE_CHOICE;
wenzelm [Sun, 11 Sep 2011 19:52:09 +0200] rev 44880
explicit choice of interface;
wenzelm [Sun, 11 Sep 2011 17:30:01 +0200] rev 44879
more orthogonal signature;
wenzelm [Sun, 11 Sep 2011 15:20:09 +0200] rev 44878
updates for release;
wenzelm [Sun, 11 Sep 2011 14:58:52 +0200] rev 44877
misc tuning and clarification (NB: settings are already local for named snapshots/releases);
wenzelm [Sun, 11 Sep 2011 14:42:15 +0200] rev 44876
some updates of PLATFORMS;
wenzelm [Sun, 11 Sep 2011 13:27:22 +0200] rev 44875
more README;
wenzelm [Sat, 10 Sep 2011 23:28:58 +0200] rev 44874
merged
krauss [Sat, 10 Sep 2011 22:43:17 +0200] rev 44873
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
wenzelm [Sat, 10 Sep 2011 23:27:32 +0200] rev 44872
misc tuning;
wenzelm [Sat, 10 Sep 2011 22:11:55 +0200] rev 44871
misc tuning and clarification;
wenzelm [Sat, 10 Sep 2011 21:47:55 +0200] rev 44870
speed up slow proof;
wenzelm [Sat, 10 Sep 2011 20:41:27 +0200] rev 44869
merged
haftmann [Sat, 10 Sep 2011 19:44:41 +0200] rev 44868
more modularization
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"