Changes

Summary

merged
"split add" -> "split"

Changeset 7014:72ff4ae9ce87 by nipkow: merged
Changeset 7013:bf70254cb1a3 by nipkow: "split add" -> "split"
The file was modified	`thys/Abortable_Linearizable_Modules/Simulations.thy` (diff)
The file was modified	`thys/Abstract-Hoare-Logics/Proc/PHoareTotal.thy` (diff)
The file was modified	`thys/Abstract-Hoare-Logics/Procs/PsHoareTotal.thy` (diff)
The file was modified	`thys/Abstract-Hoare-Logics/While/HoareTotal.thy` (diff)
The file was modified	`thys/CISC-Kernel/step/Step_invariants.thy` (diff)
The file was modified	`thys/CISC-Kernel/step/Step_vpeq_locally_respects.thy` (diff)
The file was modified	`thys/CISC-Kernel/step/Step_vpeq_weakly_step_consistent.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/CISK.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/Separation_kernel_model.thy` (diff)
The file was modified	`thys/FOL-Fitting/FOL_Fitting.thy` (diff)
The file was modified	`thys/FileRefinement/FileRefinement.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/DolevYao/Event.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/DolevYao/Public.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/GeneralAttacker/EventGA.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/GeneralAttacker/PublicGA.thy` (diff)
The file was modified	`thys/Jinja/BV/BVExample.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/TF_JVM.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Correctness1.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/Orders.thy` (diff)
The file was modified	`thys/MiniML/W.thy` (diff)
The file was modified	`thys/POPLmark-deBruijn/Basis.thy` (diff)
The file was modified	`thys/POPLmark-deBruijn/POPLmark.thy` (diff)
The file was modified	`thys/POPLmark-deBruijn/POPLmarkRecord.thy` (diff)
The file was modified	`thys/Presburger-Automata/Presburger_Automata.thy` (diff)
The file was modified	`thys/Tail_Recursive_Functions/CaseStudy2.thy` (diff)