<commit_before>(*  Title:      HOL/ex/sorting.ML
    ID:         $Id$
    Author:     <NAME>
    Copyright   1994 TU Muenchen

Some general lemmas
*)

Goal "multiset (xs@ys) x = multiset xs x + multiset ys x";
by (induct_tac "xs" 1);
by Auto_tac;
qed "multiset_append";

Goal "multiset [x:xs. ~p(x)] x + multiset [x:xs. p(x)] x = multiset xs x";
by (induct_tac "xs" 1);
by Auto_tac;
qed "multiset_compl_add";

Addsimps [multiset_append, multiset_compl_add];

Goal "set xs = {x. multiset xs x ~= 0}";
by (induct_tac "xs" 1);<commit_msg>renamed a variable to avoid possible free/bound confusion<commit_after>(*  Title:      HOL/ex/sorting.ML
    ID:         $Id$
    Author:     <NAME>
    Copyright   1994 TU Muenchen

Some general lemmas
*)

Goal "multiset (xs@ys) x = multiset xs x + multiset ys x";
by (induct_tac "xs" 1);
by Auto_tac;
qed "multiset_append";

Goal "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z";
by (induct_tac "xs" 1);
by Auto_tac;
qed "multiset_compl_add";

Addsimps [multiset_append, multiset_compl_add];

Goal "set xs = {x. multiset xs x ~= 0}";
by (induct_tac "xs" 1);
{'fraction_non_alphanumeric': 0.14272890484739678, 'fraction_numerical': 0.01436265709156194, 'mean_word_length': 3.6265560165975104, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6921191', 'n_tokens_mistral': 517, 'n_tokens_neox': 468, 'n_words': 140}