src/HOL/Tools/Metis/metis_translate.ML
changeset 42745 b817c6f91a98
parent 42727 f365f5138771
child 42758 865ce93ce025
equal deleted inserted replaced
42744:59753d5448e0 42745:b817c6f91a98
   530 
   530 
   531 fun string_of_mode FO = "FO"
   531 fun string_of_mode FO = "FO"
   532   | string_of_mode HO = "HO"
   532   | string_of_mode HO = "HO"
   533   | string_of_mode FT = "FT"
   533   | string_of_mode FT = "FT"
   534 
   534 
   535 fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
   535 fun fn_isa_to_met_sublevel "equal" = "c_fequal"
   536   | fn_isa_to_met_sublevel "c_False" = "c_fFalse"
   536   | fn_isa_to_met_sublevel "c_False" = "c_fFalse"
   537   | fn_isa_to_met_sublevel "c_True" = "c_fTrue"
   537   | fn_isa_to_met_sublevel "c_True" = "c_fTrue"
   538   | fn_isa_to_met_sublevel "c_Not" = "c_fNot"
   538   | fn_isa_to_met_sublevel "c_Not" = "c_fNot"
   539   | fn_isa_to_met_sublevel "c_conj" = "c_fconj"
   539   | fn_isa_to_met_sublevel "c_conj" = "c_fconj"
   540   | fn_isa_to_met_sublevel "c_disj" = "c_fdisj"
   540   | fn_isa_to_met_sublevel "c_disj" = "c_fdisj"