equal
deleted
inserted
replaced
75 val length_0_conv = thm "length_0_conv"; |
75 val length_0_conv = thm "length_0_conv"; |
76 val length_Suc_conv = thm "length_Suc_conv"; |
76 val length_Suc_conv = thm "length_Suc_conv"; |
77 val length_append = thm "length_append"; |
77 val length_append = thm "length_append"; |
78 val length_butlast = thm "length_butlast"; |
78 val length_butlast = thm "length_butlast"; |
79 val length_drop = thm "length_drop"; |
79 val length_drop = thm "length_drop"; |
80 val length_filter = thm "length_filter"; |
80 val length_filter_le = thm "length_filter_le"; |
81 val length_greater_0_conv = thm "length_greater_0_conv"; |
81 val length_greater_0_conv = thm "length_greater_0_conv"; |
82 val length_induct = thm "length_induct"; |
82 val length_induct = thm "length_induct"; |
83 val length_list_update = thm "length_list_update"; |
83 val length_list_update = thm "length_list_update"; |
84 val length_map = thm "length_map"; |
84 val length_map = thm "length_map"; |
85 val length_replicate = thm "length_replicate"; |
85 val length_replicate = thm "length_replicate"; |