Fri, 07 May 2010 14:47:09 +0200 wenzelm merged
Fri, 07 May 2010 09:59:59 +0200 haftmann merged
Fri, 07 May 2010 09:59:24 +0200 haftmann prefix normalizing replaces class_semiring
Thu, 06 May 2010 23:37:07 +0200 haftmann xsymbolized
Thu, 06 May 2010 23:11:58 +0200 haftmann moved method syntax here
Thu, 06 May 2010 23:11:58 +0200 haftmann tuned proof
Thu, 06 May 2010 23:11:57 +0200 haftmann former free-floating field_comp_conv now in structure Normalizer
Thu, 06 May 2010 23:11:57 +0200 haftmann proper sublocales; no free-floating ML sections
Thu, 06 May 2010 23:11:56 +0200 haftmann moved some lemmas from Groebner_Basis here
Thu, 06 May 2010 19:35:43 +0200 haftmann revert to loose merge semantics
Thu, 06 May 2010 19:27:51 +0200 haftmann merged
Thu, 06 May 2010 18:16:07 +0200 haftmann moved generic lemmas to appropriate places
Thu, 06 May 2010 17:59:20 +0200 haftmann tuned
Thu, 06 May 2010 17:59:19 +0200 haftmann dropped duplicate comp_arith
Thu, 06 May 2010 17:55:12 +0200 haftmann avoid open; tuned references to theorems
Thu, 06 May 2010 17:55:11 +0200 haftmann avoid references to groebner bases in names which have no references to groebner bases
Thu, 06 May 2010 17:09:18 +0200 haftmann tuned whitespace
Thu, 06 May 2010 17:06:47 +0200 haftmann tuned headings
Thu, 06 May 2010 17:02:34 +0200 haftmann avoid open
Thu, 06 May 2010 17:00:46 +0200 haftmann tuned internal structure
Thu, 06 May 2010 16:57:59 +0200 haftmann fail on merge of conflicting normalization entries: functions are not mergable
Thu, 06 May 2010 16:57:28 +0200 haftmann more canonical data administration
Thu, 06 May 2010 16:53:35 +0200 haftmann removed former algebra presimpset entirely
Thu, 06 May 2010 16:50:26 +0200 haftmann removed former algebra presimpset from accessor
Thu, 06 May 2010 16:41:14 +0200 haftmann removed former algebra presimpset from signature
Thu, 06 May 2010 16:40:02 +0200 haftmann moved presimplification rules for algebraic methods into named thms functor
Thu, 06 May 2010 16:32:21 +0200 haftmann tuned whitespace; dropped superfluous open
Thu, 06 May 2010 16:32:20 +0200 haftmann dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
Wed, 05 May 2010 16:53:21 +0200 haftmann moved nat_arith ot Nat_Numeral: clarified normalizer setup
Wed, 05 May 2010 16:46:19 +0200 haftmann dropped unused file
Wed, 05 May 2010 16:46:18 +0200 haftmann dropped Id
Thu, 06 May 2010 11:08:19 -0700 huffman remove unused constant preal_of_rat; remove several unused lemmas about preals
Thu, 06 May 2010 14:22:05 +0200 Cezary Kaliszyk respectfullness and preservation of prod_rel
Thu, 06 May 2010 10:55:09 +0200 haftmann ProofContext.init_global
Thu, 06 May 2010 08:44:19 +0200 haftmann merged
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Thu, 06 May 2010 08:43:51 +0200 haftmann constant name access lattice is not in use any longer
Thu, 06 May 2010 23:57:55 +0200 wenzelm uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
Thu, 06 May 2010 23:52:20 +0200 wenzelm replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
Thu, 06 May 2010 23:32:29 +0200 wenzelm added separate;
Thu, 06 May 2010 23:07:21 +0200 wenzelm basic formatting of pretty trees;
Thu, 06 May 2010 22:54:25 +0200 wenzelm added content_length;
Thu, 06 May 2010 21:02:34 +0200 wenzelm slightly more general Library.chunks;
Thu, 06 May 2010 17:49:57 +0200 wenzelm misc tuning -- accumulate body via ListBuffer;
Thu, 06 May 2010 16:27:47 +0200 wenzelm basic support for symbolic pretty printing;
Thu, 06 May 2010 15:04:37 +0200 wenzelm extractors for document updates;
Thu, 06 May 2010 13:41:30 +0200 wenzelm extractors for outer keyword declarations;
Wed, 05 May 2010 23:55:29 +0200 wenzelm eliminated deprecated "--" method;
Wed, 05 May 2010 23:41:59 +0200 wenzelm use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;
Wed, 05 May 2010 23:22:11 +0200 wenzelm use SwingApplication instead of deprecated GUIApplication;
Wed, 05 May 2010 23:09:34 +0200 wenzelm simplified via Position extractors;
Wed, 05 May 2010 22:23:45 +0200 wenzelm some rearrangement of Scala sources;
Wed, 05 May 2010 15:30:01 +0200 Cezary Kaliszyk fminus and some more theorems ported from Finite_Set.
Wed, 05 May 2010 09:24:42 +0200 haftmann eq_morphism is always optional: avoid trivial morphism for empty list of equations
Wed, 05 May 2010 09:24:41 +0200 haftmann tuned whitespace
Wed, 05 May 2010 08:57:23 +0200 haftmann tuned interpunctation, dropped dead comment
Tue, 04 May 2010 21:04:04 -0700 huffman merged
Tue, 04 May 2010 21:03:50 -0700 huffman avoid using '...' with LIMSEQ (cf. 1cc4ab4b7ff7)
Tue, 04 May 2010 19:53:57 -0700 huffman generalize some lemmas to class t1_space
Tue, 04 May 2010 19:23:59 -0700 huffman simplify definition of t1_space; generalize lemma closed_sing and related lemmas
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip