2010-08-28 haftmann [Sat, 28 Aug 2010 16:14:32 +0200] rev 38864
formerly unnamed infix equality now named HOL.eq
NEWS src/HOL/Decision_Procs/Approximation.thy src/HOL/Decision_Procs/Dense_Linear_Order.thy src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy src/HOL/Decision_Procs/commutative_ring_tac.ML src/HOL/Decision_Procs/ferrante_rackoff.ML src/HOL/Decision_Procs/langford.ML src/HOL/HOL.thy src/HOL/Import/Generate-HOLLight/GenHOLLight.thy src/HOL/Import/HOLLight/hollight.imp src/HOL/Import/hol4rews.ML src/HOL/Import/proof_kernel.ML src/HOL/Import/shuffler.ML src/HOL/Library/OptionalSugar.thy src/HOL/Library/reflection.ML src/HOL/Mutabelle/Mutabelle.thy src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/Set.thy src/HOL/Statespace/distinct_tree_prover.ML src/HOL/Statespace/state_fun.ML src/HOL/Statespace/state_space.ML src/HOL/Tools/Datatype/datatype_abs_proofs.ML src/HOL/Tools/Datatype/datatype_codegen.ML src/HOL/Tools/Function/termination.ML src/HOL/Tools/Nitpick/minipick.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_model.ML src/HOL/Tools/Nitpick/nitpick_mono.ML src/HOL/Tools/Nitpick/nitpick_nut.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML src/HOL/Tools/Predicate_Compile/code_prolog.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/Qelim/qelim.ML src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/Quotient/quotient_term.ML src/HOL/Tools/SMT/smt_monomorph.ML src/HOL/Tools/SMT/smt_normalize.ML src/HOL/Tools/SMT/smtlib_interface.ML src/HOL/Tools/SMT/z3_interface.ML src/HOL/Tools/SMT/z3_proof_literals.ML src/HOL/Tools/SMT/z3_proof_tools.ML src/HOL/Tools/Sledgehammer/clausifier.ML src/HOL/Tools/Sledgehammer/metis_clauses.ML src/HOL/Tools/Sledgehammer/metis_tactics.ML src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML ...

2010-08-30 haftmann [Mon, 30 Aug 2010 09:28:02 +0200] rev 38863
code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin
src/Tools/Code/code_haskell.ML src/Tools/Code/code_ml.ML src/Tools/Code/code_scala.ML src/Tools/Code/code_target.ML

2010-08-30 Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 30 Aug 2010 15:52:09 +0900] rev 38862
Quotient Package: dont unfold mem_def, use rsp and prs instead
src/HOL/Tools/Quotient/quotient_tacs.ML

2010-08-30 Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 30 Aug 2010 15:44:33 +0900] rev 38861
Quotient Package: added respectfulness and preservation lemmas for mem.
src/HOL/Quotient.thy

2010-08-28 Christian Urban <urbanc@in.tum.de> [Sat, 28 Aug 2010 21:17:25 +0800] rev 38860
quotient package: added a list of pre-simplification rules for Ball, Bex and mem
src/HOL/Tools/Quotient/quotient_tacs.ML

2010-08-28 Christian Urban <urbanc@in.tum.de> [Sat, 28 Aug 2010 20:24:40 +0800] rev 38859
quotient package: lemmas to be lifted and descended can be pre-simplified
src/HOL/Quotient.thy src/HOL/Tools/Quotient/quotient_tacs.ML

2010-08-28 haftmann [Sat, 28 Aug 2010 11:42:33 +0200] rev 38858
merged
NEWS src/HOL/String.thy

2010-08-27 haftmann [Fri, 27 Aug 2010 19:34:23 +0200] rev 38857
renamed class/constant eq to equal; tuned some instantiations
NEWS doc-src/Codegen/Thy/Foundations.thy src/HOL/Code_Evaluation.thy src/HOL/Code_Numeral.thy src/HOL/HOL.thy src/HOL/Int.thy src/HOL/Lazy_Sequence.thy src/HOL/Library/AssocList.thy src/HOL/Library/Code_Char.thy src/HOL/Library/Code_Integer.thy src/HOL/Library/Code_Natural.thy src/HOL/Library/Dlist.thy src/HOL/Library/Efficient_Nat.thy src/HOL/Library/Enum.thy src/HOL/Library/Fset.thy src/HOL/Library/List_Prefix.thy src/HOL/Library/List_lexord.thy src/HOL/Library/Mapping.thy src/HOL/Library/Multiset.thy src/HOL/Library/Nested_Environment.thy src/HOL/Library/Polynomial.thy src/HOL/Library/Product_ord.thy src/HOL/Library/RBT.thy src/HOL/List.thy src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Option.thy src/HOL/Predicate.thy src/HOL/Product_Type.thy src/HOL/Quickcheck.thy src/HOL/Rat.thy src/HOL/RealDef.thy src/HOL/String.thy src/HOL/Tools/Datatype/datatype_codegen.ML src/HOL/Tools/Nitpick/nitpick.ML src/HOL/Tools/hologic.ML src/HOL/Tools/record.ML src/HOL/Typerep.thy src/HOL/Word/Word.thy src/HOL/ex/Numeral.thy

2010-08-27 haftmann [Fri, 27 Aug 2010 15:36:02 +0200] rev 38856
improved deresolving of implicits
src/Tools/Code/code_scala.ML

2010-08-30 wenzelm [Mon, 30 Aug 2010 10:36:55 +0200] rev 38855
Document_View.text_area_extension: do not insist in crashing if (weak) assertion is violated;
src/Tools/jEdit/src/jedit/document_view.scala