1signature ppc_Lib = 2sig 3 include Abbrev 4 5 val ppc_decode : string -> thm 6 val ppc_step : string -> thm 7 8 val ppc_test : string -> (string * string) list -> (string * string) list -> thm 9 10end 11