isabelle update -u control_cartouches;

clarified signature: prefer proper order operation;

tuned signature;
eliminated clones;

tuned signature;

abstract type Name_Space.table;
clarified pretty_locale_deps: sort strings;
clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;

formal cleanup of sources

tuned;

removing debug code in mutabelle

removing dead code from Mutabelle; tuned

quickcheck invocations in mutabelle must not catch codegenerator errors internally

moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms

adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle

standardized some ML aliases;

modernized structure Proof_Context;

adapting mutabelle; exporting more Quickcheck functions

adapting mutabelle

adjusting HOL-Mutabelle to changes in quickcheck

tuned comments;

eliminated some hard tabulators (deprecated);

adapting mutabelle

adapting mutabelle

adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle

adapting HOL-Mutabelle to changes in quickcheck

renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;

renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;

--HG--
rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML

discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;

tuned titles

prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";

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 =)

renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

modernized structure Object_Logic;

modernized structure Term_Ord;

Changed author; removed debugging code.

adding Mutabelle to repository