equal
deleted
inserted
replaced
166 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm' |
166 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm' |
167 | Or_to_List => "Or_to_List " |
167 | Or_to_List => "Or_to_List " |
168 |
168 |
169 | Empty_Tac => "Empty_Tac" |
169 | Empty_Tac => "Empty_Tac" |
170 (*RM*)| Tac string => "Tac " ^ string(*RM*) |
170 (*RM*)| Tac string => "Tac " ^ string(*RM*) |
171 | End_Proof' => "input End_Proof'" |
171 | End_Proof' => "input End_Proof'"; |
172 | _ => "input_to_string not impl. for ?!"; |
|
173 |
172 |
174 fun tac2IDstr ma = case ma of |
173 fun tac2IDstr ma = case ma of |
175 Model_Problem => "Model_Problem" |
174 Model_Problem => "Model_Problem" |
176 | Refine_Tacitly _ => "Refine_Tacitly" |
175 | Refine_Tacitly _ => "Refine_Tacitly" |
177 | Refine_Problem _ => "Refine_Problem" |
176 | Refine_Problem _ => "Refine_Problem" |