Changes

Summary

First step to remove nonstandard "[x <- xs. P]" syntax: only input
merged
removed unicode symbol
Moved Landau_Symbols from the AFP to HOL-Library

Changeset 68249:949d93804740 by nipkow: First step to remove nonstandard "[x <- xs. P]" syntax: only input
The file was modified	`NEWS` (diff)
The file was modified	`src/Doc/Isar_Ref/Inner_Syntax.thy` (diff)
The file was modified	`src/Doc/Main/Main_Doc.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/AB.thy` (diff)
The file was modified	`src/HOL/Library/AList.thy` (diff)
The file was modified	`src/HOL/Library/Finite_Map.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/List.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Kildall.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/LBVComplete.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/LBVCorrect.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/LBVSpec.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/SemilatAlg.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Manual_Nits.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/W.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Quotient_FSet.thy` (diff)
The file was modified	`src/HOL/Random.thy` (diff)
The file was modified	`src/HOL/ex/Quicksort.thy` (diff)
The file was modified	`src/HOL/ex/Radix_Sort.thy` (diff)
Changeset 68248:ef1e0cb80fde by nipkow: merged
Changeset 68247:7344affc0bd4 by nipkow: removed unicode symbol
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
Changeset 68246:b48bab511939 by manuel eberl _eberlm@in.tum.de_: Moved Landau_Symbols from the AFP to HOL-Library
The file was added	`src/HOL/Library/Landau_Symbols.thy`
The file was modified	`CONTRIBUTORS` (diff)
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Library/Library.thy` (diff)