integrate new rule in pattern completeness algorithm, refactoring
Showing
- thys/Pattern_Completeness/Finite_IDL_Solver_Interface.thy 44 additions, 0 deletionsthys/Pattern_Completeness/Finite_IDL_Solver_Interface.thy
- thys/Pattern_Completeness/Pattern_Completeness.thy 9 additions, 9 deletionsthys/Pattern_Completeness/Pattern_Completeness.thy
- thys/Pattern_Completeness/Pattern_Completeness_List.thy 692 additions, 486 deletionsthys/Pattern_Completeness/Pattern_Completeness_List.thy
- thys/Pattern_Completeness/Pattern_Completeness_Multiset.thy 4 additions, 0 deletionsthys/Pattern_Completeness/Pattern_Completeness_Multiset.thy
- thys/Pattern_Completeness/Pattern_Completeness_Set.thy 84 additions, 0 deletionsthys/Pattern_Completeness/Pattern_Completeness_Set.thy
- thys/Pattern_Completeness/ROOT 3 additions, 0 deletionsthys/Pattern_Completeness/ROOT
- thys/Pattern_Completeness/Singleton_List.thy 20 additions, 0 deletionsthys/Pattern_Completeness/Singleton_List.thy
- thys/Pattern_Completeness/Test_Pat_Complete.thy 22 additions, 8 deletionsthys/Pattern_Completeness/Test_Pat_Complete.thy
Loading
Please register or sign in to comment