changeset 33420 | 17b7095ad463 |
parent 33187 | 616be6d7997e |
child 33943 | f31d645b4e00 |
child 33955 | fff6f11b1f09 |
child 33990 | febc68c02b63 |
--- a/src/Tools/Code/code_thingol.ML Mon Nov 02 18:49:53 2009 -0800 +++ b/src/Tools/Code/code_thingol.ML Tue Nov 03 17:06:08 2009 +0100 @@ -261,7 +261,8 @@ | NONE => (case Code.get_datatype_of_constr thy c of SOME dtco => Codegen.thyname_of_type thy dtco | NONE => Codegen.thyname_of_const thy c); - fun purify_base "op &" = "and" + fun purify_base "==>" = "follows" + | purify_base "op &" = "and" | purify_base "op |" = "or" | purify_base "op -->" = "implies" | purify_base "op :" = "member"