Changes

Summary

merged
fix (non-existent) document generation
updated to scala-2.12.7;
news
de-emphasize HOL-SPARK: somewhat outdated;
proper naming conventions for contexts;
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
tuned spelling;
tuned whitespace and sections;
tuned -- eliminated clone;
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
obsolete (see 6f8ae6ddc26b);
updated to new list_update precedence
avoid confusing precedences

Changeset 69097:e65ab21821bf by immler: merged
Changeset 69096:62a0d10386c1 by immler: fix (non-existent) document generation
The file was modified	`src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy` (diff)
Changeset 69095:39b248fb20a2 by wenzelm: updated to scala-2.12.7;
The file was modified	`Admin/components/components.sha1` (diff)
The file was modified	`Admin/components/main` (diff)
Changeset 69094:b96dd4963e2d by nipkow: news
The file was modified	`NEWS` (diff)
Changeset 69093:b28ad89d8a50 by wenzelm: de-emphasize HOL-SPARK: somewhat outdated;
The file was modified	`src/HOL/ROOT` (diff)
Changeset 69092:854bd35cad49 by wenzelm: proper naming conventions for contexts;
The file was modified	`src/HOL/Tools/Lifting/lifting_info.ML` (diff)
Changeset 69091:ce62fd14961a by wenzelm: permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
The file was modified	`src/HOL/Tools/Lifting/lifting_info.ML` (diff)
Changeset 69090:1b656a2ec0ad by wenzelm: tuned spelling;
The file was modified	`src/HOL/Tools/Lifting/lifting_info.ML` (diff)
Changeset 69089:43dade957d59 by wenzelm: tuned whitespace and sections;
The file was modified	`src/HOL/Tools/Lifting/lifting_info.ML` (diff)
Changeset 69088:051127c38be8 by wenzelm: tuned -- eliminated clone;
The file was modified	`src/HOL/Tools/Lifting/lifting_info.ML` (diff)
Changeset 69087:06017b2c4552 by wenzelm: suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
The file was modified	`src/Pure/Isar/experiment.ML` (diff)
The file was modified	`src/Pure/Thy/export_theory.ML` (diff)
Changeset 69086:2859dcdbc849 by wenzelm: obsolete (see 6f8ae6ddc26b);
The file was modified	`src/Pure/Thy/export_theory.ML` (diff)
Changeset 69085:9999d7823b8f by nipkow: updated to new list_update precedence
The file was modified	`src/HOL/Computational_Algebra/Formal_Power_Series.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/ex/SatChecker.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/ex/Subarray.thy` (diff)
The file was modified	`src/HOL/MicroJava/Comp/CorrCompTp.thy` (diff)
The file was modified	`src/HOL/MicroJava/Comp/Index.thy` (diff)
Changeset 69084:c7c38c901267 by nipkow: avoid confusing precedences
The file was modified	`src/HOL/List.thy` (diff)