2009-09-11 Thomas Sewell <tsewell@nicta.com.au> [Fri, 11 Sep 2009 20:58:29 +1000] rev 32749
Implement previous fix (don't duplicate ext_def) correctly.
src/HOL/Tools/record.ML

2009-09-11 Thomas Sewell <tsewell@nicta.com.au> [Fri, 11 Sep 2009 18:03:30 +1000] rev 32748
There's no particular reason to duplicate the extension
constant's definition under the name "ext_def", and it
also prevents you having a field called ext.
src/HOL/Tools/record.ML

2009-09-11 Thomas Sewell <tsewell@nicta.com.au> [Fri, 11 Sep 2009 15:57:16 +1000] rev 32747
Merged with mainline changes.
lib/Tools/codegen lib/Tools/jedit lib/scripts/mirabelle src/HOL/Library/Legacy_GCD.thy src/HOL/Library/Pocklington.thy src/HOL/Library/Primes.thy src/HOL/NewNumberTheory/Binomial.thy src/HOL/NewNumberTheory/Cong.thy src/HOL/NewNumberTheory/Fib.thy src/HOL/NewNumberTheory/MiscAlgebra.thy src/HOL/NewNumberTheory/ROOT.ML src/HOL/NewNumberTheory/Residues.thy src/HOL/NewNumberTheory/UniqueFactorization.thy src/HOL/NumberTheory/BijectionRel.thy src/HOL/NumberTheory/Chinese.thy src/HOL/NumberTheory/Euler.thy src/HOL/NumberTheory/EulerFermat.thy src/HOL/NumberTheory/EvenOdd.thy src/HOL/NumberTheory/Factorization.thy src/HOL/NumberTheory/Fib.thy src/HOL/NumberTheory/Finite2.thy src/HOL/NumberTheory/Gauss.thy src/HOL/NumberTheory/Int2.thy src/HOL/NumberTheory/IntFact.thy src/HOL/NumberTheory/IntPrimes.thy src/HOL/NumberTheory/Quadratic_Reciprocity.thy src/HOL/NumberTheory/ROOT.ML src/HOL/NumberTheory/Residues.thy src/HOL/NumberTheory/WilsonBij.thy src/HOL/NumberTheory/WilsonRuss.thy src/HOL/NumberTheory/document/root.tex src/HOL/Tools/ComputeFloat.thy src/HOL/Tools/ComputeHOL.thy src/HOL/Tools/ComputeNumeral.thy src/HOL/ex/Mirabelle.thy src/HOL/ex/mirabelle.ML src/Pure/Isar/isar.scala src/Pure/Tools/isabelle_syntax.scala

2009-09-11 Thomas Sewell <tsewell@nicta.com.au> [Fri, 11 Sep 2009 15:56:51 +1000] rev 32746
Adjust some documentation.
src/HOL/IsTuple.thy

2009-09-10 Thomas Sewell <tsewell@nicta.com.au> [Thu, 10 Sep 2009 16:38:18 +1000] rev 32745
Simplification of various aspects of the IsTuple component
of the new record package. Extensive documentation added in
IsTuple.thy - it should now be possible to figure out what's
going on from the sources supplied.
src/HOL/IsTuple.thy src/HOL/Record.thy src/HOL/Tools/istuple_support.ML src/HOL/Tools/record.ML

2009-09-10 Thomas Sewell <tsewell@nicta.com.au> [Thu, 10 Sep 2009 15:18:43 +1000] rev 32744
Record patch imported and working.
src/HOL/IsTuple.thy src/HOL/Record.thy src/HOL/Tools/istuple_support.ML src/HOL/Tools/record.ML

2009-08-27 tsewell@rubicon.NSW.bigpond.net.au [Thu, 27 Aug 2009 00:40:53 +1000] rev 32743
Initial attempt at porting record update to repository Isabelle.
src/HOL/IsTuple.thy src/HOL/Record.thy src/HOL/Tools/istuple_support.ML src/HOL/Tools/record.ML

2009-09-29 wenzelm [Tue, 29 Sep 2009 16:42:29 +0200] rev 32742
Synchronized and Unsynchronized;
NEWS

2009-09-29 wenzelm [Tue, 29 Sep 2009 16:42:02 +0200] rev 32741
hide "ref" by default, to enforce excplicit indication as Unsynchronized;
src/Pure/ML-Systems/polyml_common.ML

2009-09-29 wenzelm [Tue, 29 Sep 2009 16:24:36 +0200] rev 32740
explicit indication of Unsynchronized.ref;
src/CCL/ROOT.ML src/FOLP/IFOLP.thy src/FOLP/simp.ML src/HOL/Code_Evaluation.thy src/HOL/Decision_Procs/cooper_tac.ML src/HOL/Decision_Procs/ferrack_tac.ML src/HOL/Decision_Procs/mir_tac.ML src/HOL/Fun.thy src/HOL/HOL.thy src/HOL/Import/hol4rews.ML src/HOL/Import/import.ML src/HOL/Import/import_syntax.ML src/HOL/Import/importrecorder.ML src/HOL/Import/lazy_seq.ML src/HOL/Import/proof_kernel.ML src/HOL/Import/shuffler.ML src/HOL/Library/Eval_Witness.thy src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML src/HOL/Library/positivstellensatz.ML src/HOL/Matrix/cplex/Cplex_tools.ML src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML src/HOL/Modelcheck/EindhovenSyn.thy src/HOL/Modelcheck/mucke_oracle.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/Prolog/prolog.ML src/HOL/Random.thy src/HOL/SMT/Tools/smt_normalize.ML src/HOL/Statespace/DistinctTreeProver.thy src/HOL/Tools/ATP_Manager/atp_manager.ML src/HOL/Tools/ATP_Manager/atp_minimal.ML src/HOL/Tools/ATP_Manager/atp_wrapper.ML src/HOL/Tools/Function/fundef_common.ML src/HOL/Tools/Function/scnp_solve.ML src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/cnf_funcs.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/meson.ML src/HOL/Tools/polyhash.ML src/HOL/Tools/prop_logic.ML src/HOL/Tools/quickcheck_generators.ML src/HOL/Tools/record.ML src/HOL/Tools/res_axioms.ML src/HOL/Tools/sat_funcs.ML src/HOL/Tools/sat_solver.ML ...