31 } 
31 } 
32 
32 
33 my %convert_kinds = ( 
33 my %convert_kinds = ( 
34 "thy_begin" => "theorybegin", 
34 "thy_begin" => "theorybegin", 
35 "thy_end" => "theoryend", 
35 "thy_end" => "theoryend", 
36 "thy_heading" => "theoryheading", 
36 "thy_heading1" => "theoryheading", 

37 "thy_heading2" => "theoryheading", 

38 "thy_heading3" => "theoryheading", 

39 "thy_heading4" => "theoryheading", 
37 "thy_decl" => "theorydecl", 
40 "thy_decl" => "theorydecl", 
38 "thy_script" => "theoryscript", 
41 "thy_script" => "theoryscript", 
39 "thy_goal" => "theorygoal", 
42 "thy_goal" => "theorygoal", 
40 "thy_schematic_goal" => "theorygoal", 
43 "thy_schematic_goal" => "theorygoal", 
41 "qed_block" => "qedblock", 
44 "qed_block" => "qedblock", 
42 "qed_global" => "qedglobal", 
45 "qed_global" => "qedglobal", 
43 "prf_heading" => "proofheading", 
46 "prf_heading2" => "proofheading", 

47 "prf_heading3" => "proofheading", 

48 "prf_heading4" => "proofheading", 
44 "prf_goal" => "proofgoal", 
49 "prf_goal" => "proofgoal", 
45 "prf_block" => "proofblock", 
50 "prf_block" => "proofblock", 
46 "prf_open" => "proofopen", 
51 "prf_open" => "proofopen", 
47 "prf_close" => "proofclose", 
52 "prf_close" => "proofclose", 
48 "prf_chain" => "proofchain", 
53 "prf_chain" => "proofchain", 