src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 57461 29efe682335b
parent 57460 9cc802a8ab06
child 57462 dabd4516450d
equal deleted inserted replaced
57460:9cc802a8ab06 57461:29efe682335b
   539 
   539 
   540 val encode_str = String.translate meta_char
   540 val encode_str = String.translate meta_char
   541 val decode_str = String.explode #> unmeta_chars []
   541 val decode_str = String.explode #> unmeta_chars []
   542 
   542 
   543 val encode_strs = map encode_str #> space_implode " "
   543 val encode_strs = map encode_str #> space_implode " "
   544 val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
   544 val decode_strs = space_explode " " #> map decode_str
   545 
   545 
   546 datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
   546 datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
   547 
   547 
   548 fun str_of_proof_kind Isar_Proof = "i"
   548 fun str_of_proof_kind Isar_Proof = "i"
   549   | str_of_proof_kind Automatic_Proof = "a"
   549   | str_of_proof_kind Automatic_Proof = "a"