[Hol-checkins] [mn200/HOL] 1566a4: replace add_persistent_funs with a LoadableThyData...

[GitHub <no...@gi...>]

  Branch: refs/heads/persistent_funs
  Home:   https://github.com/mn200/HOL
  Commit: 1566a4c33ff61da5736aeb53c90509aa8595cfc5
      https://github.com/mn200/HOL/commit/1566a4c33ff61da5736aeb53c90509aa8595cfc5
  Author: Ramana Kumar <ram...@gm...>
  Date:   2012-07-29 (Sun, 29 Jul 2012)

  Changed paths:
    M src/compute/src/computeLib.sml

  Log Message:
  -----------
  replace add_persistent_funs with a LoadableThyData version

Progress on #73. Haven't touched the "del" variant yet: ThmSetData has
less support for deleting at the moment, and not sure what is actually
necessary.


  Commit: 898866fa84444c3942272a348aac5c6c83d3a60d
      https://github.com/mn200/HOL/commit/898866fa84444c3942272a348aac5c6c83d3a60d
  Author: Ramana Kumar <ram...@gm...>
  Date:   2012-07-29 (Sun, 29 Jul 2012)

  Changed paths:
    M src/tfl/src/Defn.sml

  Log Message:
  -----------
  make Defn.add_persistent_funs play nice with new compLib version (#73)

compLib.add_persistent_funs previously accepted a string that was
arbitrary code to be printed at the end of a theory. Now it must be the
name of a theorem in the current theory.

Defn was running SUC_TO_NUMERAL_DEFN_CONV in the printed code; now it
saves a theorem with the result of the conversion and uses its name
instead.


Compare: https://github.com/mn200/HOL/compare/1566a4c33ff6^...898866fa8444