equal
deleted
inserted
replaced
189 end |
189 end |
190 end |
190 end |
191 |
191 |
192 fun eqvt_transform ctxt thm = |
192 fun eqvt_transform ctxt thm = |
193 case (prop_of thm) of |
193 case (prop_of thm) of |
194 @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ |
194 @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ |
195 (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => |
195 (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => |
196 eqvt_transform_eq ctxt thm |
196 eqvt_transform_eq ctxt thm |
197 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => |
197 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => |
198 eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt |
198 eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt |
199 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." |
199 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." |