changeset 57229 | 489083abce44 |
parent 56245 | 84fc7dfa3cd4 |
child 57230 | ec5ff6bb2a92 |
--- a/src/HOL/Tools/SMT2/smt2_util.ML Thu Jun 12 01:00:49 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_util.ML Thu Jun 12 01:00:49 2014 +0200 @@ -59,7 +59,7 @@ val under_quant_conv: (Proof.context * cterm list -> conv) -> Proof.context -> conv val prop_conv: conv -> conv -end +end; structure SMT2_Util: SMT2_UTIL = struct @@ -221,4 +221,4 @@ @{const Trueprop} $ _ => Conv.arg_conv cv ct | _ => raise CTERM ("not a property", [ct])) -end +end;