2013-05-13 wenzelm [Mon, 13 May 2013 13:23:13 +0200] rev 51960
option "goals_limit", with more uniform description;
etc/options src/Doc/IsarRef/Document_Preparation.thy src/Doc/IsarRef/Inner_Syntax.thy src/Pure/Isar/isar_syn.ML src/Pure/ProofGeneral/preferences.ML src/Pure/goal_display.ML

2013-05-13 wenzelm [Mon, 13 May 2013 13:01:10 +0200] rev 51959
clarified message when subgoals have been stripped -- unconditional;
src/Pure/goal_display.ML

2013-05-13 wenzelm [Mon, 13 May 2013 12:40:17 +0200] rev 51958
retain goal display options when printing error messages, to avoid breakdown for huge goals;
src/HOL/Tools/Function/lexicographic_order.ML src/Pure/Isar/proof_display.ML src/Pure/Thy/thy_output.ML src/Pure/goal.ML src/Pure/goal_display.ML

2013-05-13 kuncar [Mon, 13 May 2013 15:22:19 +0200] rev 51957
typo
src/HOL/Tools/Lifting/lifting_def.ML

2013-05-13 kuncar [Mon, 13 May 2013 13:59:04 +0200] rev 51956
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
src/HOL/Library/Quotient_List.thy src/HOL/Library/Quotient_Option.thy src/HOL/Library/Quotient_Product.thy src/HOL/Library/Quotient_Set.thy src/HOL/Library/Quotient_Sum.thy src/HOL/Lifting.thy src/HOL/Rat.thy src/HOL/Real.thy src/HOL/Tools/Lifting/lifting_setup.ML src/HOL/Tools/transfer.ML src/HOL/Transfer.thy src/HOL/ex/Transfer_Int_Nat.thy

2013-05-13 kuncar [Mon, 13 May 2013 12:13:24 +0200] rev 51955
try to detect assumptions of transfer rules that are in a shape of a transfer rule
src/HOL/Tools/transfer.ML src/HOL/Transfer.thy

2013-05-13 kuncar [Mon, 13 May 2013 12:13:24 +0200] rev 51954
publish a private function
src/HOL/Tools/transfer.ML

2013-05-13 nipkow [Mon, 13 May 2013 06:50:37 +0200] rev 51953
tuned names
src/HOL/IMP/Abs_Int3.thy

2013-05-12 wenzelm [Sun, 12 May 2013 20:58:01 +0200] rev 51952
re-init ISABELLE_PROCESS_OPTIONS to allow nested ISABELLE_PROCESS invocations, e.g. HOL-Mutabelle-ex;
bin/isabelle-process

2013-05-12 wenzelm [Sun, 12 May 2013 20:46:17 +0200] rev 51951
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML src/HOL/Tools/Metis/metis_reconstruct.ML src/Pure/PIDE/markup.ML src/Pure/System/options.ML