equal
deleted
inserted
replaced
5 natural numbers and numerals. |
5 natural numbers and numerals. |
6 *) |
6 *) |
7 |
7 |
8 signature MULTISET_SIMPROCS = |
8 signature MULTISET_SIMPROCS = |
9 sig |
9 sig |
10 val subset_cancel_msets: Proof.context -> cterm -> thm option |
10 val subset_cancel_msets: Simplifier.proc |
11 val subseteq_cancel_msets: Proof.context -> cterm -> thm option |
11 val subseteq_cancel_msets: Simplifier.proc |
12 end; |
12 end; |
13 |
13 |
14 structure Multiset_Simprocs : MULTISET_SIMPROCS = |
14 structure Multiset_Simprocs : MULTISET_SIMPROCS = |
15 struct |
15 struct |
16 |
16 |