equal
deleted
inserted
replaced
122 Const (\<^const_name>\<open>times\<close>, _) $ num $ t1' => (* 3*_a_ \<up> 2 *) |
122 Const (\<^const_name>\<open>times\<close>, _) $ num $ t1' => (* 3*_a_ \<up> 2 *) |
123 if TermC.is_atom num andalso TermC.is_atom t1' then Free_to_string t2 |
123 if TermC.is_atom num andalso TermC.is_atom t1' then Free_to_string t2 |
124 else "|||||||||||||" |
124 else "|||||||||||||" |
125 | _ => |
125 | _ => |
126 (case t2 of |
126 (case t2 of |
127 Const (\<^const_name>\<open>powr\<close>, _) $ base $ exp => |
127 Const (\<^const_name>\<open>realpow\<close>, _) $ base $ exp => |
128 if TermC.is_atom base andalso TermC.is_atom exp then |
128 if TermC.is_atom base andalso TermC.is_atom exp then |
129 if TermC.is_num base then "|||||||||||||" |
129 if TermC.is_num base then "|||||||||||||" |
130 else Free_to_string base |
130 else Free_to_string base |
131 else "|||||||||||||" |
131 else "|||||||||||||" |
132 | _ => "|||||||||||||")) |
132 | _ => "|||||||||||||")) |
133 | identifier (Const (\<^const_name>\<open>powr\<close>, _) $ base $ exp) = (* _a_\<up>2, _3_^2 *) |
133 | identifier (Const (\<^const_name>\<open>realpow\<close>, _) $ base $ exp) = (* _a_\<up>2, _3_^2 *) |
134 if TermC.is_atom base andalso TermC.is_atom exp then Free_to_string base |
134 if TermC.is_atom base andalso TermC.is_atom exp then Free_to_string base |
135 else "|||||||||||||" |
135 else "|||||||||||||" |
136 | identifier t = (* 12 *) |
136 | identifier t = (* 12 *) |
137 if TermC.is_num t |
137 if TermC.is_num t |
138 then TermC.string_of_num t |
138 then TermC.string_of_num t |
163 if TermC.is_atom t then true |
163 if TermC.is_atom t then true |
164 else |
164 else |
165 case t of |
165 case t of |
166 Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ t1 $ t2 => |
166 Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ t1 $ t2 => |
167 ist_monom t1 andalso ist_monom t2 |
167 ist_monom t1 andalso ist_monom t2 |
168 | Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ t1 $ t2 => |
168 | Const (\<^const_name>\<open>realpow\<close>, _) $ t1 $ t2 => |
169 ist_monom t1 andalso ist_monom t2 |
169 ist_monom t1 andalso ist_monom t2 |
170 | _ => false |
170 | _ => false |
171 |
171 |
172 (* is this a univariate monomial ? *) |
172 (* is this a univariate monomial ? *) |
173 (*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*) |
173 (*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*) |