src/HOL/Tools/Function/pat_completeness.ML
changeset 37744 3daaf23b9ab4
parent 36945 9bec62c10714
child 42361 23f352990944
equal deleted inserted replaced
37743:0a3fa8fbcdc5 37744:3daaf23b9ab4
     1 (*  Title:      HOL/Tools/Function/fundef_datatype.ML
     1 (*  Title:      HOL/Tools/Function/pat_completeness.ML
     2     Author:     Alexander Krauss, TU Muenchen
     2     Author:     Alexander Krauss, TU Muenchen
     3 
     3 
     4 Method "pat_completeness" to prove completeness of datatype patterns.
     4 Method "pat_completeness" to prove completeness of datatype patterns.
     5 *)
     5 *)
     6 
     6