src/Pure/Tools/find_theorems.ML
changeset 56914 f371418b9641
parent 56912 293cd4dcfebc
child 57690 5b652fd305d4
equal deleted inserted replaced
56913:df4cd6e1fdfa 56914:f371418b9641
    68     | Elim => Pretty.str (prfx "elim")
    68     | Elim => Pretty.str (prfx "elim")
    69     | Dest => Pretty.str (prfx "dest")
    69     | Dest => Pretty.str (prfx "dest")
    70     | Solves => Pretty.str (prfx "solves")
    70     | Solves => Pretty.str (prfx "solves")
    71     | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
    71     | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
    72         Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))]
    72         Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))]
    73     | Pattern pat => Pretty.enclose (prfx " \"") "\""
    73     | Pattern pat => Pretty.enclose (prfx "\"") "\""
    74         [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)])
    74         [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)])
    75   end;
    75   end;
    76 
    76 
    77 
    77 
    78 
    78