Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

Fix ImpSplit thy for document generation
Add B+Tree formalisation to the BTree entry

Changeset 12915:22f95a29b159 by Niels Mündler _n.muendler@web.de_: Fix ImpSplit thy for document generation
The file was modified	`thys/BTree/BPlusTree_ImpSplit.thy`
Changeset 12914:b5b59c822549 by Niels Mündler _n.muendler@web.de_: Add B+Tree formalisation to the BTree entry
The file was added	`thys/BTree/BPlusTree.thy`
The file was added	`thys/BTree/BPlusTree_Imp.thy`
The file was added	`thys/BTree/BPlusTree_ImpRange.thy`
The file was added	`thys/BTree/BPlusTree_ImpSet.thy`
The file was added	`thys/BTree/BPlusTree_ImpSplit.thy`
The file was added	`thys/BTree/BPlusTree_ImpSplitCE.thy`
The file was added	`thys/BTree/BPlusTree_Iter.thy`
The file was added	`thys/BTree/BPlusTree_Iter_OneWay.thy`
The file was added	`thys/BTree/BPlusTree_Range.thy`
The file was added	`thys/BTree/BPlusTree_Set.thy`
The file was added	`thys/BTree/BPlusTree_Split.thy`
The file was added	`thys/BTree/BPlusTree_SplitCE.thy`
The file was added	`thys/BTree/Flatten_Iter.thy`
The file was added	`thys/BTree/Flatten_Iter_Spec.thy`
The file was added	`thys/BTree/Imp_List_Sum.thy`
The file was added	`thys/BTree/Inst_Ex_Assn.thy`
The file was added	`thys/BTree/LICENSE`
The file was added	`thys/BTree/Partially_Filled_Array_Iter.thy`
The file was added	`thys/BTree/Subst_Mod_Mult_AC.thy`
The file was added	`thys/BTree/inst_ex_assn.ML`
The file was modified	`metadata/entries/BTree.toml`
The file was modified	`thys/BTree/Array_SBlit.thy`
The file was modified	`thys/BTree/Basic_Assn.thy`
The file was modified	`thys/BTree/Imperative_Loops.thy`
The file was modified	`thys/BTree/Partially_Filled_Array.thy`
The file was modified	`thys/BTree/README.md`
The file was modified	`thys/BTree/ROOT`
The file was modified	`thys/BTree/document/root.tex`