Changes

Summary

merged
used List.sorted_wrt
VerifyThis2018 fully adapted from Isabelle 2017 to Isabelle dev
ported several parts in VerifyThis2018 from Isabelle 2017 to Isabelle-dev

Changeset 9216:8c4f6bd7601e by nipkow: merged
Changeset 9215:b29e57192844 by nipkow: used List.sorted_wrt
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/Collections/GenCF/Gen/Gen_Map2Set.thy` (diff)
The file was modified	`thys/Collections/GenCF/Impl/Impl_RBT_Map.thy` (diff)
The file was modified	`thys/Collections/GenCF/Intf/Intf_Set.thy` (diff)
The file was modified	`thys/Collections/ICF/ICF_Autoref.thy` (diff)
The file was modified	`thys/Collections/ICF/ICF_Refine_Monadic.thy` (diff)
The file was modified	`thys/Collections/Iterator/Gen_Iterator.thy` (diff)
The file was modified	`thys/Collections/Iterator/Proper_Iterator.thy` (diff)
The file was modified	`thys/Collections/Iterator/SetAbstractionIterator.thy` (diff)
The file was modified	`thys/Collections/Iterator/SetIterator.thy` (diff)
The file was modified	`thys/Collections/Iterator/SetIteratorGA.thy` (diff)
The file was modified	`thys/Collections/Iterator/SetIteratorOperations.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/IICF_Sepl_Binding.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Foreach.thy` (diff)
Changeset 9214:a0ff6f42fdb8 by rene thiemann _rene.thiemann@uibk.ac.at_: VerifyThis2018 fully adapted from Isabelle 2017 to Isabelle dev
The file was modified	`thys/VerifyThis2018/Challenge3.thy` (diff)
Changeset 9213:ac7b825b42fa by rene thiemann _rene.thiemann@uibk.ac.at_: ported several parts in VerifyThis2018 from Isabelle 2017 to Isabelle-dev
The file was modified	`thys/VerifyThis2018/Challenge1.thy` (diff)
The file was modified	`thys/VerifyThis2018/Challenge1_short.thy` (diff)
The file was modified	`thys/VerifyThis2018/Challenge2.thy` (diff)
The file was modified	`thys/VerifyThis2018/Challenge3.thy` (diff)
The file was modified	`thys/VerifyThis2018/lib/Array_Map_Default.thy` (diff)
The file was modified	`thys/VerifyThis2018/lib/Impl_List_Set_Ndj.thy` (diff)