2014-01-26 wenzelm [Sun, 26 Jan 2014 14:01:19 +0100] rev 55152
discontinued obsolete attribute "standard";
NEWS src/Doc/IsarRef/Generic.thy src/Pure/Pure.thy

2014-01-26 wenzelm [Sun, 26 Jan 2014 13:45:40 +0100] rev 55151
tuned signature;
src/HOL/Bali/AxExample.thy src/HOL/Bali/Basis.thy src/HOL/Prolog/prolog.ML src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/HOL/Tools/TFL/post.ML src/Pure/Tools/rule_insts.ML src/ZF/ind_syntax.ML

2014-01-25 haftmann [Sat, 25 Jan 2014 23:50:49 +0100] rev 55150
less clumsy namespace
src/Tools/Code/code_haskell.ML src/Tools/Code/code_ml.ML src/Tools/Code/code_namespace.ML src/Tools/Code/code_printer.ML src/Tools/Code/code_runtime.ML src/Tools/Code/code_scala.ML src/Tools/Code/code_symbol.ML src/Tools/Code/code_target.ML src/Tools/Code/code_thingol.ML src/Tools/nbe.ML

2014-01-25 haftmann [Sat, 25 Jan 2014 23:50:49 +0100] rev 55149
immediate "activation" of const syntax at declaration time
src/Tools/Code/code_symbol.ML src/Tools/Code/code_target.ML

2014-01-25 haftmann [Sat, 25 Jan 2014 23:50:49 +0100] rev 55148
avoid (now superfluous) indirect passing of constant names
src/HOL/List.thy src/HOL/Tools/numeral.ML src/HOL/Tools/string_code.ML src/Tools/Code/code_haskell.ML src/Tools/Code/code_printer.ML

2014-01-25 haftmann [Sat, 25 Jan 2014 23:50:49 +0100] rev 55147
prefer explicit code symbol type over ad-hoc name mangling
src/Doc/Codegen/Adaptation.thy src/HOL/Imperative_HOL/Heap_Monad.thy src/HOL/List.thy src/HOL/Quickcheck_Narrowing.thy src/HOL/Quickcheck_Random.thy src/HOL/Tools/Quickcheck/narrowing_generators.ML src/HOL/Tools/numeral.ML src/HOL/Tools/string_code.ML src/Tools/Code/code_haskell.ML src/Tools/Code/code_ml.ML src/Tools/Code/code_namespace.ML src/Tools/Code/code_printer.ML src/Tools/Code/code_runtime.ML src/Tools/Code/code_scala.ML src/Tools/Code/code_simp.ML src/Tools/Code/code_symbol.ML src/Tools/Code/code_target.ML src/Tools/Code/code_thingol.ML src/Tools/nbe.ML

2014-01-25 haftmann [Sat, 25 Jan 2014 23:50:49 +0100] rev 55146
more abstract syntax passing
src/Tools/Code/code_target.ML

2014-01-25 haftmann [Sat, 25 Jan 2014 23:50:49 +0100] rev 55145
more abstract declaration of unqualified constant names in code printing context
src/Tools/Code/code_haskell.ML src/Tools/Code/code_ml.ML src/Tools/Code/code_printer.ML src/Tools/Code/code_scala.ML

2014-01-25 wenzelm [Sat, 25 Jan 2014 22:18:20 +0100] rev 55144
merged

2014-01-25 wenzelm [Sat, 25 Jan 2014 22:06:07 +0100] rev 55143
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
NEWS src/Doc/IsarRef/Proof.thy src/Doc/isar.sty src/HOL/Bali/AxExample.thy src/HOL/Bali/Basis.thy src/HOL/Library/Binomial.thy src/HOL/Number_Theory/Binomial.thy src/HOL/Prolog/prolog.ML src/HOL/Rat.thy src/HOL/Set.thy src/HOL/Set_Interval.thy src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/HOL/Tools/TFL/post.ML src/Pure/Tools/rule_insts.ML src/ZF/ind_syntax.ML