2010-05-05 haftmann [Wed, 05 May 2010 18:25:34 +0200] rev 36692
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 =)
src/FOLP/hypsubst.ML src/FOLP/simp.ML src/HOL/Decision_Procs/cooper_tac.ML src/HOL/Decision_Procs/ferrack_tac.ML src/HOL/Decision_Procs/mir_tac.ML src/HOL/HOL.thy src/HOL/Import/hol4rews.ML src/HOL/Import/proof_kernel.ML src/HOL/Import/shuffler.ML src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML src/HOL/Library/normarith.ML src/HOL/Library/reflection.ML src/HOL/Modelcheck/mucke_oracle.ML src/HOL/Mutabelle/mutabelle.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_inductive2.ML src/HOL/Statespace/state_space.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/datatype_aux.ML src/HOL/Tools/Datatype/datatype_codegen.ML src/HOL/Tools/Datatype/datatype_realizer.ML src/HOL/Tools/Function/function_common.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/Qelim/presburger.ML src/HOL/Tools/Quotient/quotient_term.ML src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/cnf_funcs.ML src/HOL/Tools/hologic.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/inductive_set.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/old_primrec.ML src/HOL/Tools/recfun_codegen.ML src/HOL/Tools/refute.ML src/HOL/Tools/sat_solver.ML src/HOL/Tools/typedef_codegen.ML src/HOLCF/IOA/ABP/Check.ML src/HOLCF/IOA/meta_theory/automaton.ML src/HOLCF/Tools/Domain/domain_library.ML src/HOLCF/Tools/Domain/domain_take_proofs.ML src/HOLCF/Tools/Domain/domain_theorems.ML src/Provers/Arith/cancel_div_mod.ML src/Provers/Arith/fast_lin_arith.ML ...

2010-05-06 haftmann [Thu, 06 May 2010 08:43:51 +0200] rev 36691
constant name access lattice is not in use any longer
doc-src/Locales/Locales/Examples.thy doc-src/Locales/Locales/document/Examples.tex

2010-05-06 wenzelm [Thu, 06 May 2010 23:57:55 +0200] rev 36690
uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
src/Pure/General/pretty.ML

2010-05-06 wenzelm [Thu, 06 May 2010 23:52:20 +0200] rev 36689
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
src/Pure/General/markup.scala src/Pure/General/pretty.ML src/Pure/General/pretty.scala src/Pure/ProofGeneral/proof_general_pgip.ML

2010-05-06 wenzelm [Thu, 06 May 2010 23:32:29 +0200] rev 36688
added separate;
src/Pure/library.scala

2010-05-06 wenzelm [Thu, 06 May 2010 23:07:21 +0200] rev 36687
basic formatting of pretty trees;
line-up ML vs. Scala sources;
src/Pure/General/pretty.ML src/Pure/General/pretty.scala

2010-05-06 wenzelm [Thu, 06 May 2010 22:54:25 +0200] rev 36686
added content_length;
src/Pure/General/xml.scala

2010-05-06 wenzelm [Thu, 06 May 2010 21:02:34 +0200] rev 36685
slightly more general Library.chunks;
src/Pure/General/yxml.scala src/Pure/library.scala

2010-05-06 wenzelm [Thu, 06 May 2010 17:49:57 +0200] rev 36684
misc tuning -- accumulate body via ListBuffer;
src/Pure/General/yxml.scala

2010-05-06 wenzelm [Thu, 06 May 2010 16:27:47 +0200] rev 36683
basic support for symbolic pretty printing;
tuned;
src/Pure/General/markup.scala src/Pure/General/position.scala src/Pure/General/pretty.scala src/Pure/build-jars