7 months ago wenzelm [Thu, 07 Dec 2017 19:36:48 +0100] rev 67157
clarified document preparation vs. skip_proofs;
NEWS src/Pure/Isar/proof.ML src/Pure/Isar/toplevel.ML

7 months ago nipkow [Thu, 07 Dec 2017 18:04:52 +0100] rev 67156
"important" annotations
src/HOL/Analysis/L2_Norm.thy

7 months ago nipkow [Thu, 07 Dec 2017 15:48:50 +0100] rev 67155
canonical name
src/HOL/Analysis/Cartesian_Euclidean_Space.thy src/HOL/Analysis/Connected.thy src/HOL/Analysis/Convex_Euclidean_Space.thy src/HOL/Analysis/Finite_Cartesian_Product.thy src/HOL/Analysis/L2_Norm.thy src/HOL/Analysis/Topology_Euclidean_Space.thy

7 months ago wenzelm [Thu, 07 Dec 2017 11:14:32 +0100] rev 67154
tuned output in isar-ref manual;
lib/texinputs/isabellesym.sty

7 months ago wenzelm [Thu, 07 Dec 2017 11:12:55 +0100] rev 67153
obsolete (used to be part of old src/Pure/codegen.ML);
lib/texinputs/isabellesym.sty

7 months ago wenzelm [Wed, 06 Dec 2017 21:43:20 +0100] rev 67152
just one session for bulky HOL-Analysis documents;
src/Doc/ROOT src/HOL/ROOT

7 months ago wenzelm [Wed, 06 Dec 2017 21:30:26 +0100] rev 67151
more default tags;
lib/texinputs/isabelle.sty src/Doc/System/Presentation.thy

7 months ago wenzelm [Wed, 06 Dec 2017 21:01:01 +0100] rev 67150
merged

7 months ago wenzelm [Wed, 06 Dec 2017 20:43:09 +0100] rev 67149
prefer control symbol antiquotations;
src/HOL/Deriv.thy src/HOL/HOL.thy src/HOL/Tools/Argo/argo_real.ML src/HOL/Tools/Argo/argo_tactic.ML src/HOL/Tools/Function/fun.ML src/HOL/Tools/Function/fun_cases.ML src/HOL/Tools/Function/function.ML src/HOL/Tools/Function/function_common.ML src/HOL/Tools/Function/function_core.ML src/HOL/Tools/Function/function_elims.ML src/HOL/Tools/Function/function_lib.ML src/HOL/Tools/Function/induction_schema.ML src/HOL/Tools/Function/lexicographic_order.ML src/HOL/Tools/Function/measure_functions.ML src/HOL/Tools/Function/mutual.ML src/HOL/Tools/Function/partial_function.ML src/HOL/Tools/Function/sum_tree.ML src/HOL/Tools/Function/termination.ML src/HOL/Tools/Meson/meson.ML src/HOL/Tools/Meson/meson_clausify.ML src/HOL/Tools/Meson/meson_tactic.ML src/HOL/Tools/Quickcheck/abstract_generators.ML src/HOL/Tools/Quickcheck/exhaustive_generators.ML src/HOL/Tools/Quickcheck/find_unused_assms.ML src/HOL/Tools/Quickcheck/narrowing_generators.ML src/HOL/Tools/Quickcheck/quickcheck_common.ML src/HOL/Tools/Quickcheck/random_generators.ML src/HOL/Tools/SMT/conj_disj_perm.ML src/HOL/Tools/SMT/smt_builtin.ML src/HOL/Tools/SMT/smt_config.ML src/HOL/Tools/SMT/smt_datatypes.ML src/HOL/Tools/SMT/smt_normalize.ML src/HOL/Tools/SMT/smt_translate.ML src/HOL/Tools/arith_data.ML src/HOL/Tools/boolean_algebra_cancel.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/cnf.ML src/HOL/Tools/code_evaluation.ML src/HOL/Tools/coinduction.ML src/HOL/Tools/functor.ML src/HOL/Tools/groebner.ML src/HOL/Tools/group_cancel.ML src/HOL/Tools/hologic.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/inductive_set.ML src/HOL/Tools/int_arith.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/monomorph.ML src/HOL/Tools/nat_arith.ML ...

7 months ago wenzelm [Wed, 06 Dec 2017 19:34:59 +0100] rev 67148
more robust, e.g. when Sidekick produces multi-selection;
src/Tools/jEdit/src/isabelle.scala