TFL/post.ML
 changeset 18678 dd0c569fa43d parent 18139 b15981aedb7b child 19736 d8d0f8f51d69
equal inserted replaced
18677:01265301db7f 18678:dd0c569fa43d
`   205 local`
`   205 local`
`   206   fun get_related_thms i = `
`   206   fun get_related_thms i = `
`   207       List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));`
`   207       List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));`
`   208 `
`   208 `
`   209   fun solve_eq (th, [], i) = `
`   209   fun solve_eq (th, [], i) = `
`   210       raise ERROR_MESSAGE "derive_init_eqs: missing rules"`
`   210         error "derive_init_eqs: missing rules"`
`   211     | solve_eq (th, [a], i) = [(a, i)]`
`   211     | solve_eq (th, [a], i) = [(a, i)]`
`   212     | solve_eq (th, splitths as (_ :: _), i) = `
`   212     | solve_eq (th, splitths as (_ :: _), i) = `
`   213       (writeln "Proving unsplit equation...";`
`   213       (writeln "Proving unsplit equation...";`
`   214       [((standard o ObjectLogic.rulify_no_asm)`
`   214       [((standard o ObjectLogic.rulify_no_asm)`
`   215           (CaseSplit.splitto splitths th), i)])`
`   215           (CaseSplit.splitto splitths th), i)])`
`   216       (* if there's an error, pretend nothing happened with this definition `
`   216       (* if there's an error, pretend nothing happened with this definition `
`   217          We should probably print something out so that the user knows...? *)`
`   217          We should probably print something out so that the user knows...? *)`
`   218       handle ERROR_MESSAGE s => `
`   218       handle ERROR s => `
`   219              (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);`
`   219              (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);`
`   220 in`
`   220 in`
`   221 fun derive_init_eqs sgn rules eqs = `
`   221 fun derive_init_eqs sgn rules eqs = `
`   222     let `
`   222     let `
`   223       val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) `
`   223       val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) `