Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. Hidden another instance of 'uncurry' clash
  3. Additional patches to accomodate for upstrea, changes
  4. merged
  5. Moved more Refinement Framework stuff upstream, improved refine_{rcg,vcg}
  6. Moved more stuff from Sepref_Misc, aligned set_rel of Refinement Framework with rel_set of transfer/lifting
  7. Moving stuff from Sepref_Misc
  8. cleaned up map_eq_appendE
  9. merged
  10. more refactoring, eliminated Sep_Misc
Changeset 8024:3a66d7c4beeb by lammich _lammich@in.tum.de_:
merged
Changeset 8023:951640995859 by lammich _lammich@in.tum.de_:
Hidden another instance of 'uncurry' clash
The file was modified thys/LOFT/LinuxRouter_OpenFlow_Translation.thy (diff)
Changeset 8022:1fd8b38c821c by lammich _lammich@in.tum.de_:
Additional patches to accomodate for upstrea, changes
The file was modified thys/DFS_Framework/Examples/DFS_Find_Path.thy (diff)
The file was modified thys/DFS_Framework/Examples/Nested_DFS.thy (diff)
The file was modified thys/Formal_SSA/Construct_SSA_code.thy (diff)
The file was modified thys/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy (diff)
The file was modified thys/Iptables_Semantics/Primitive_Matchers/Output_Interface_Replace.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Refinement/Weak_Set.thy (diff)
Changeset 8021:28bd737910f3 by lammich _lammich@in.tum.de_:
merged
Changeset 8020:69705a6955e5 by lammich _lammich@in.tum.de_:
Moved more Refinement Framework stuff upstream, improved refine_{rcg,vcg}
The file was addedthys/Refine_Monadic/Refine_More_Comb.thy
The file was modified thys/Automatic_Refinement/Lib/Misc.thy (diff)
The file was modified thys/Automatic_Refinement/Parametricity/Param_HOL.thy (diff)
The file was modified thys/Automatic_Refinement/Parametricity/Relators.thy (diff)
The file was modified thys/CAVA_Automata/CAVA_Base/CAVA_Base.thy (diff)
The file was modified thys/Collections/GenCF/Impl/Impl_List_Set.thy (diff)
The file was modified thys/DFS_Framework/Impl/Data/Restr_Impl.thy (diff)
The file was modified thys/DFS_Framework/Impl/Data/Simple_Impl.thy (diff)
The file was modified thys/DFS_Framework/Impl/Structural/General_DFS_Structure.thy (diff)
The file was modified thys/DFS_Framework/Impl/Structural/Rec_Impl.thy (diff)
The file was modified thys/DFS_Framework/Misc/DFS_Framework_Refine_Aux.thy (diff)
The file was modified thys/EdmondsKarp_Maxflow/Augmenting_Path_BFS.thy (diff)
The file was modified thys/EdmondsKarp_Maxflow/Edka_Checked_Impl.thy (diff)
The file was modified thys/EdmondsKarp_Maxflow/EdmondsKarp_Algo.thy (diff)
The file was modified thys/EdmondsKarp_Maxflow/Fofu_Impl_Base.thy (diff)
The file was modified thys/EdmondsKarp_Maxflow/FordFulkerson_Algo.thy (diff)
The file was modified thys/EdmondsKarp_Maxflow/Refine_Add_Fofu.thy (diff)
The file was modified thys/Gabow_SCC/Gabow_GBG.thy (diff)
The file was modified thys/Gabow_SCC/Gabow_SCC.thy (diff)
The file was modified thys/Gabow_SCC/Gabow_Skeleton.thy (diff)
The file was modified thys/LTL_to_GBA/LTL_to_GBA.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Examples/Sepref_NDFS.thy (diff)
The file was modified thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Abs_Heap.thy (diff)
The file was modified thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Abs_Heapmap.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Lib/Sepref_Misc.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Sepref_Basic.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Sepref_HOL_Bindings.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Sepref_Rules.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Sepref_Translate.thy (diff)
The file was modified thys/Refine_Monadic/Generic/RefineG_Recursion.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Automation.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Basic.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Foreach.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Heuristics.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Leof.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Monadic.thy (diff)
The file was modified thys/Refine_Monadic/Refine_While.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Assertions.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Automation.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Examples/Array_Blit.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Hoare_Triple.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Run.thy (diff)
The file was removedthys/EdmondsKarp_Maxflow/Refine_Monadic_Syntax_Sugar.thy
Changeset 8019:3aa9a7023455 by lammich _lammich@in.tum.de_:
Moved more stuff from Sepref_Misc, aligned set_rel of Refinement Framework with rel_set of transfer/lifting
The file was addedthys/Automatic_Refinement/Lib/Refine_Util_Bootstrap1.thy
The file was modified thys/Automatic_Refinement/Autoref_Bindings_HOL.thy (diff)
The file was modified thys/Automatic_Refinement/Lib/Mk_Term_Antiquot.thy (diff)
The file was modified thys/Automatic_Refinement/Lib/Mpat_Antiquot.thy (diff)
The file was modified thys/Automatic_Refinement/Lib/Refine_Util.thy (diff)
The file was modified thys/Automatic_Refinement/Parametricity/Param_HOL.thy (diff)
The file was modified thys/Automatic_Refinement/Parametricity/Relators.thy (diff)
The file was modified thys/DFS_Framework/Impl/Structural/General_DFS_Structure.thy (diff)
The file was modified thys/Floyd_Warshall/FW_Code.thy (diff)
The file was modified thys/Refine_Imperative_HOL/IICF/Impl/IICF_Sepl_Binding.thy (diff)
The file was modified thys/Refine_Imperative_HOL/IICF/Intf/IICF_Map.thy (diff)
The file was modified thys/Refine_Imperative_HOL/IICF/Intf/IICF_Multiset.thy (diff)
The file was modified thys/Refine_Imperative_HOL/IICF/Intf/IICF_Set.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Lib/Sepref_Misc.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Sepref_HOL_Bindings.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Sepref_ICF_Bindings.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_Reference.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Misc.thy (diff)
Changeset 8018:f15f18c592c9 by lammich _lammich@in.tum.de_:
Moving stuff from Sepref_Misc
The file was modified thys/Automatic_Refinement/Lib/Misc.thy (diff)
The file was modified thys/Automatic_Refinement/Lib/Refine_Util.thy (diff)
The file was modified thys/Automatic_Refinement/Parametricity/Param_HOL.thy (diff)
The file was modified thys/Automatic_Refinement/ROOT (diff)
The file was modified thys/Refine_Imperative_HOL/Lib/Sepref_Misc.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Sepref_Rules.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Foreach.thy (diff)
The file was modified thys/Refine_Monadic/TODO (diff)
Changeset 8017:a54c698f2bea by lammich _lammich@in.tum.de_:
cleaned up map_eq_appendE
The file was modified thys/Automatic_Refinement/Lib/Misc.thy (diff)
The file was modified thys/Collections/GenCF/Gen/Gen_Map.thy (diff)
The file was modified thys/EdmondsKarp_Maxflow/Graph.thy (diff)
Changeset 8016:8257bafdef1f by lammich _lammich@in.tum.de_:
merged
Changeset 8015:a05274a330cd by lammich _lammich@in.tum.de_:
more refactoring, eliminated Sep_Misc
The file was modified thys/Automatic_Refinement/Lib/Misc.thy (diff)
The file was modified thys/Collections/GenCF/Impl/Impl_List_Map.thy (diff)
The file was modified thys/Collections/ICF/impl/HashMap_Impl.thy (diff)
The file was modified thys/Collections/ICF/impl/ListMapImpl.thy (diff)
The file was modified thys/Collections/ICF/impl/ListMapImpl_Invar.thy (diff)
The file was modified thys/Collections/ICF/impl/RBTMapImpl.thy (diff)
The file was modified thys/Collections/ICF/impl/TrieMapImpl.thy (diff)
The file was modified thys/Collections/Lib/Diff_Array.thy (diff)
The file was modified thys/Collections/Lib/Robdd.thy (diff)
The file was modified thys/Refine_Imperative_HOL/IICF/Intf/IICF_Map.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Lib/Sepref_Misc.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Det.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Assertions.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Examples/Array_Blit.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Examples/Circ_List.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Examples/Open_List.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/ROOT (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Tools/Imperative_HOL_Add.thy (diff)
The file was removedthys/Separation_Logic_Imperative_HOL/Tools/Sep_Misc.thy