Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. just one session for bulky HOL-Analysis documents;
  2. more default tags;
  3. merged
  4. prefer control symbol antiquotations;
  5. more robust, e.g. when Sidekick produces multi-selection;
  6. prefer control symbol antiquotations;
  7. more embedded cartouche arguments; more uniform LaTeX output for control symbols;
  8. name mangling for Latex macros; tuned signature;
  9. removed (un)important tags again to make latex happy
  10. initial version of Analysis document
  11. tuned
Changeset 67152:8021ea06aad8 by wenzelm:
just one session for bulky HOL-Analysis documents;
The file was modified src/Doc/ROOT (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 67151:d1ace598c026 by wenzelm:
more default tags;
The file was modified lib/texinputs/isabelle.sty (diff)
The file was modified src/Doc/System/Presentation.thy (diff)
Changeset 67150:ecbd8ff928c5 by wenzelm:
merged
Changeset 67149:e61557884799 by wenzelm:
prefer control symbol antiquotations;
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Tools/Argo/argo_real.ML (diff)
The file was modified src/HOL/Tools/Argo/argo_tactic.ML (diff)
The file was modified src/HOL/Tools/Function/fun.ML (diff)
The file was modified src/HOL/Tools/Function/fun_cases.ML (diff)
The file was modified src/HOL/Tools/Function/function.ML (diff)
The file was modified src/HOL/Tools/Function/function_common.ML (diff)
The file was modified src/HOL/Tools/Function/function_core.ML (diff)
The file was modified src/HOL/Tools/Function/function_elims.ML (diff)
The file was modified src/HOL/Tools/Function/function_lib.ML (diff)
The file was modified src/HOL/Tools/Function/induction_schema.ML (diff)
The file was modified src/HOL/Tools/Function/lexicographic_order.ML (diff)
The file was modified src/HOL/Tools/Function/measure_functions.ML (diff)
The file was modified src/HOL/Tools/Function/mutual.ML (diff)
The file was modified src/HOL/Tools/Function/partial_function.ML (diff)
The file was modified src/HOL/Tools/Function/sum_tree.ML (diff)
The file was modified src/HOL/Tools/Function/termination.ML (diff)
The file was modified src/HOL/Tools/Meson/meson.ML (diff)
The file was modified src/HOL/Tools/Meson/meson_clausify.ML (diff)
The file was modified src/HOL/Tools/Meson/meson_tactic.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/abstract_generators.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/exhaustive_generators.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/find_unused_assms.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/quickcheck_common.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/random_generators.ML (diff)
The file was modified src/HOL/Tools/SMT/conj_disj_perm.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_builtin.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_config.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_datatypes.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_normalize.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_translate.ML (diff)
The file was modified src/HOL/Tools/arith_data.ML (diff)
The file was modified src/HOL/Tools/boolean_algebra_cancel.ML (diff)
The file was modified src/HOL/Tools/choice_specification.ML (diff)
The file was modified src/HOL/Tools/cnf.ML (diff)
The file was modified src/HOL/Tools/code_evaluation.ML (diff)
The file was modified src/HOL/Tools/coinduction.ML (diff)
The file was modified src/HOL/Tools/functor.ML (diff)
The file was modified src/HOL/Tools/groebner.ML (diff)
The file was modified src/HOL/Tools/group_cancel.ML (diff)
The file was modified src/HOL/Tools/hologic.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/inductive_realizer.ML (diff)
The file was modified src/HOL/Tools/inductive_set.ML (diff)
The file was modified src/HOL/Tools/int_arith.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)
The file was modified src/HOL/Tools/monomorph.ML (diff)
The file was modified src/HOL/Tools/nat_arith.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/HOL/Tools/sat.ML (diff)
The file was modified src/HOL/Tools/split_rule.ML (diff)
The file was modified src/HOL/Tools/try0.ML (diff)
The file was modified src/HOL/Tools/typedef.ML (diff)
The file was modified src/HOL/Tools/value_command.ML (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
The file was modified src/Tools/atomize_elim.ML (diff)
The file was modified src/Tools/case_product.ML (diff)
The file was modified src/Tools/coherent.ML (diff)
The file was modified src/Tools/eqsubst.ML (diff)
The file was modified src/Tools/induct.ML (diff)
The file was modified src/Tools/induct_tacs.ML (diff)
The file was modified src/Tools/induction.ML (diff)
The file was modified src/Tools/nbe.ML (diff)
The file was modified src/Tools/quickcheck.ML (diff)
The file was modified src/Tools/solve_direct.ML (diff)
The file was modified src/Tools/subtyping.ML (diff)
The file was modified src/Tools/try.ML (diff)
Changeset 67148:d24dcac5eb4c by wenzelm:
more robust, e.g. when Sidekick produces multi-selection;
The file was modified src/Tools/jEdit/src/isabelle.scala (diff)
Changeset 67147:dea94b1aabc3 by wenzelm:
prefer control symbol antiquotations;
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/Isar/calculation.ML (diff)
The file was modified src/Pure/Isar/class.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Pure/Isar/context_rules.ML (diff)
The file was modified src/Pure/Isar/isar_cmd.ML (diff)
The file was modified src/Pure/Isar/locale.ML (diff)
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/Isar/overloading.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/ML/ml_thms.ML (diff)
The file was modified src/Pure/ML_Bootstrap.thy (diff)
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Thy/term_style.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
The file was modified src/Pure/Tools/bibtex.ML (diff)
The file was modified src/Pure/Tools/find_theorems.ML (diff)
The file was modified src/Pure/Tools/jedit.ML (diff)
The file was modified src/Pure/Tools/named_theorems.ML (diff)
The file was modified src/Pure/Tools/plugin.ML (diff)
The file was modified src/Pure/Tools/rail.ML (diff)
The file was modified src/Pure/Tools/rule_insts.ML (diff)
The file was modified src/Pure/Tools/simplifier_trace.ML (diff)
The file was modified src/Pure/simplifier.ML (diff)
Changeset 67146:909dcdec2122 by wenzelm:
more embedded cartouche arguments;<br>more uniform LaTeX output for control symbols;
The file was modified lib/texinputs/isabelle.sty (diff)
The file was modified lib/texinputs/isabellesym.sty (diff)
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/Doc/Implementation/ML.thy (diff)
The file was modified src/Doc/Implementation/Prelim.thy (diff)
The file was modified src/Doc/Isar_Ref/Inner_Syntax.thy (diff)
The file was modified src/Doc/Isar_Ref/document/showsymbols (diff)
The file was modified src/Pure/ML/ml_antiquotation.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/Tools/named_theorems.ML (diff)
The file was modified src/Pure/Tools/plugin.ML (diff)
The file was modified src/Pure/simplifier.ML (diff)
Changeset 67145:e77c5bfca9aa by wenzelm:
name mangling for Latex macros;<br>tuned signature;
The file was modified NEWS (diff)
The file was modified src/Pure/Thy/latex.ML (diff)
Changeset 67144:cef9a1514ed0 by nipkow:
removed (un)important tags again to make latex happy
The file was modified src/HOL/Analysis/L2_Norm.thy (diff)
Changeset 67143:db609ac2c307 by nipkow:
initial version of Analysis document
The file was modified src/Doc/ROOT (diff)
The file was modified src/HOL/Analysis/L2_Norm.thy (diff)
The file was modified src/HOL/Analysis/document/root.tex (diff)
Changeset 67142:fa1173288322 by nipkow:
tuned
The file was modified src/HOL/Word/Bit_Representation.thy (diff)