src/HOL/List.thy
 changeset 69215 ab94035ba6ea parent 69203 a5c0d61ce5db child 69275 9bbd5497befd
equal inserted replaced
69214:74455459973d 69215:ab94035ba6ea
`   917         val neq_len = HOLogic.mk_Trueprop (HOLogic.Not \$ eq_len);`
`   917         val neq_len = HOLogic.mk_Trueprop (HOLogic.Not \$ eq_len);`
`   918         val thm = Goal.prove ctxt [] [] neq_len`
`   918         val thm = Goal.prove ctxt [] [] neq_len`
`   919           (K (simp_tac (put_simpset ss ctxt) 1));`
`   919           (K (simp_tac (put_simpset ss ctxt) 1));`
`   920       in SOME (thm RS @{thm neq_if_length_neq}) end`
`   920       in SOME (thm RS @{thm neq_if_length_neq}) end`
`   921   in`
`   921   in`
`   922     if m < n andalso submultiset (aconv) (ls,rs) orelse`
`   922     if m < n andalso submultiset (op aconv) (ls,rs) orelse`
`   923        n < m andalso submultiset (aconv) (rs,ls)`
`   923        n < m andalso submultiset (op aconv) (rs,ls)`
`   924     then prove_neq() else NONE`
`   924     then prove_neq() else NONE`
`   925   end;`
`   925   end;`
`   926 in K list_neq end;`
`   926 in K list_neq end`
`   927 \<close>`
`   927 \<close>`
`   928 `
`   928 `
`   929 `
`   929 `
`   930 subsubsection \<open>\<open>@\<close> -- append\<close>`
`   930 subsubsection \<open>\<open>@\<close> -- append\<close>`
`   931 `
`   931 `
`  1072       in`
`  1072       in`
`  1073         if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}`
`  1073         if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}`
`  1074         else if lastl aconv lastr then rearr @{thm append_same_eq}`
`  1074         else if lastl aconv lastr then rearr @{thm append_same_eq}`
`  1075         else NONE`
`  1075         else NONE`
`  1076       end;`
`  1076       end;`
`  1077   in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end;`
`  1077   in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end`
`  1078 \<close>`
`  1078 \<close>`
`  1079 `
`  1079 `
`  1080 `
`  1080 `
`  1081 subsubsection \<open>@{const map}\<close>`
`  1081 subsubsection \<open>@{const map}\<close>`
`  1082 `
`  1082 `