equal
deleted
inserted
replaced
302 subsection \<open>Tactics for type checking\<close> |
302 subsection \<open>Tactics for type checking\<close> |
303 |
303 |
304 ML \<open> |
304 ML \<open> |
305 local |
305 local |
306 |
306 |
307 fun is_rigid_elem (Const(\<^const_name>\<open>Elem\<close>,_) $ a $ _) = not(is_Var (head_of a)) |
307 fun is_rigid_elem \<^Const_>\<open>Elem for a _\<close> = not(is_Var (head_of a)) |
308 | is_rigid_elem (Const(\<^const_name>\<open>Eqelem\<close>,_) $ a $ _ $ _) = not(is_Var (head_of a)) |
308 | is_rigid_elem \<^Const_>\<open>Eqelem for a _ _\<close> = not(is_Var (head_of a)) |
309 | is_rigid_elem (Const(\<^const_name>\<open>Type\<close>,_) $ a) = not(is_Var (head_of a)) |
309 | is_rigid_elem \<^Const_>\<open>Type for a\<close> = not(is_Var (head_of a)) |
310 | is_rigid_elem _ = false |
310 | is_rigid_elem _ = false |
311 |
311 |
312 in |
312 in |
313 |
313 |
314 (*Try solving a:A or a=b:A by assumption provided a is rigid!*) |
314 (*Try solving a:A or a=b:A by assumption provided a is rigid!*) |