src/HOL/Library/Multiset.thy
changeset 37163 f69efa106feb
parent 37091 1535aa1c943a
child 37260 8a89fd40ed0b
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu May 27 16:42:03 2010 +0200
     1.3 @@ -1699,7 +1699,6 @@
     1.4    by (fact multiset_order.less_asym)
     1.5  
     1.6  ML {*
     1.7 -(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
     1.8  fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T]))
     1.9                        (Const _ $ t') =
    1.10      let
    1.11 @@ -1727,4 +1726,4 @@
    1.12  Nitpick.register_term_postprocessor @{typ "'a multiset"} multiset_postproc
    1.13  *}
    1.14  
    1.15 -end
    1.16 \ No newline at end of file
    1.17 +end