2009-03-08 wenzelm [Sun, 08 Mar 2009 17:37:18 +0100] rev 30365
adapted to structure Long_Name;
doc-src/IsarImplementation/Thy/Prelim.thy doc-src/IsarImplementation/Thy/document/Prelim.tex doc-src/antiquote_setup.ML

2009-03-08 wenzelm [Sun, 08 Mar 2009 17:26:14 +0100] rev 30364
moved basic algebra of long names from structure NameSpace to Long_Name;
src/HOL/Import/hol4rews.ML src/HOL/Nominal/nominal_fresh_fun.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_inductive2.ML src/HOL/Nominal/nominal_package.ML src/HOL/Nominal/nominal_permeq.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/Statespace/state_fun.ML src/HOL/Statespace/state_space.ML src/HOL/Tools/TFL/post.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/datatype_abs_proofs.ML src/HOL/Tools/datatype_aux.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/datatype_prop.ML src/HOL/Tools/datatype_realizer.ML src/HOL/Tools/datatype_rep_proofs.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/function_package/size.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/old_primrec_package.ML src/HOL/Tools/primrec_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/record_package.ML src/HOL/Tools/res_atp.ML src/HOL/Tools/res_axioms.ML src/HOL/Tools/specification_package.ML src/HOL/ex/Quickcheck_Generators.thy src/HOLCF/Tools/domain/domain_axioms.ML src/HOLCF/Tools/domain/domain_extender.ML src/HOLCF/Tools/domain/domain_syntax.ML src/HOLCF/Tools/domain/domain_theorems.ML src/HOLCF/Tools/fixrec_package.ML src/Pure/Isar/class_target.ML src/Pure/Isar/element.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/proof_display.ML src/Pure/Isar/rule_cases.ML src/Pure/Isar/theory_target.ML src/Pure/ML/ml_antiquote.ML src/Pure/Proof/extraction.ML src/Pure/Proof/proof_syntax.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/Syntax/syntax.ML src/Pure/Syntax/type_ext.ML src/Pure/Thy/thm_deps.ML src/Pure/Tools/find_theorems.ML src/Pure/axclass.ML ...

2009-03-08 wenzelm [Sun, 08 Mar 2009 17:19:15 +0100] rev 30363
proper local context for text with antiquotations;
src/HOL/Algebra/Ideal.thy src/HOL/Algebra/Lattice.thy src/HOL/Algebra/UnivPoly.thy

2009-03-08 wenzelm [Sun, 08 Mar 2009 17:05:43 +0100] rev 30362
more explicit warning message;
src/HOL/Tools/metis_tools.ML

2009-03-08 wenzelm [Sun, 08 Mar 2009 17:03:07 +0100] rev 30361
added qualified_name -- emulates old-style qualified bstring;
tuned;
src/Pure/General/binding.ML

2009-03-08 wenzelm [Sun, 08 Mar 2009 16:53:38 +0100] rev 30360
added General/long_name.ML;
src/Pure/General/ROOT.ML src/Pure/IsaMakefile

2009-03-08 wenzelm [Sun, 08 Mar 2009 16:53:07 +0100] rev 30359
moved basic algebra of long names from structure NameSpace to Long_Name;
tuned signature;
src/Pure/General/long_name.ML src/Pure/General/name_space.ML

2009-03-08 wenzelm [Sun, 08 Mar 2009 15:01:10 +0100] rev 30358
index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
doc-src/antiquote_setup.ML

2009-03-08 wenzelm [Sun, 08 Mar 2009 12:16:12 +0100] rev 30357
proper context for Simplifier.pretty_ss;
src/Pure/Isar/code.ML src/Pure/Isar/isar_cmd.ML

2009-03-08 wenzelm [Sun, 08 Mar 2009 12:15:58 +0100] rev 30356
added dest_ss;
proper context fo pretty_ss;
tuned;
src/Pure/meta_simplifier.ML src/Pure/simplifier.ML