summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Fri, 15 Sep 2000 15:48:41 +0200 | |

changeset 9971 | e0164f01d55a |

parent 9970 | dfe4747c8318 |

child 9972 | 05afcc505da3 |

renamed the select rules

NEWS | file | annotate | diff | comparison | revisions | |

TFL/thms.sml | file | annotate | diff | comparison | revisions |

--- a/NEWS Fri Sep 15 15:30:50 2000 +0200 +++ b/NEWS Fri Sep 15 15:48:41 2000 +0200 @@ -31,7 +31,7 @@ f.simps instead of f.rules; * HOL: theory Sexp now in HOL/Induct examples (it used to be part of -main HOL, but was unused); should better use HOL's datatype package +main HOL, but was unused); it is better to use HOL's datatype package anyway; * HOL: removed obsolete theorem binding expand_if (refer to split_if @@ -39,6 +39,16 @@ * HOL: less_induct is renamed nat_less_induct +* HOL: systematic renaming of the @-rules: + selectI -> someI + selectI2 -> someI2 + selectI2EX -> someI2_ex + select_equality -> some_equality + select1_equality -> some1_equality + select_eq_Ex -> some_eq_ex + Eps_eq -> some_eq_trivial + Eps_sym_eq -> some_sym_eq_trivial + * HOL/Real: "rabs" replaced by overloaded "abs" function; * HOL/ML: even fewer consts are declared as global (see theories Ord,

--- a/TFL/thms.sml Fri Sep 15 15:30:50 2000 +0200 +++ b/TFL/thms.sml Fri Sep 15 15:48:41 2000 +0200 @@ -22,7 +22,7 @@ val CUT_DEF = get_thm WF.thy "cut_def"; val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)" - (fn _ => [strip_tac 1, rtac selectI 1, assume_tac 1]); + (fn _ => [strip_tac 1, rtac someI 1, assume_tac 1]); fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);