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

author | nipkow |

Fri, 20 Feb 1998 17:56:51 +0100 | |

changeset 4641 | 70a50c2a920f |

parent 4640 | ac6cf9f18653 |

child 4642 | 2d3910d6ab10 |

Congruence rules use == in premises now.

src/HOL/Integ/Bin.ML | file | annotate | diff | comparison | revisions | |

src/HOL/MiniML/Instance.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Integ/Bin.ML Fri Feb 20 17:56:39 1998 +0100 +++ b/src/HOL/Integ/Bin.ML Fri Feb 20 17:56:51 1998 +0100 @@ -230,7 +230,6 @@ by (ALLGOALS(asm_simp_tac (simpset() addsimps[zminus_zadd_distrib RS sym, znat_add RS sym]))); - by (stac eq_False_conv 1); by (rtac notI 1); by (dres_inst_tac [("f","(% z. z + $# Suc (Suc (n + n)))")] arg_cong 1); by (Asm_full_simp_tac 1);

--- a/src/HOL/MiniML/Instance.ML Fri Feb 20 17:56:39 1998 +0100 +++ b/src/HOL/MiniML/Instance.ML Fri Feb 20 17:56:51 1998 +0100 @@ -220,15 +220,8 @@ by (type_scheme.induct_tac "sch" 1); by (Simp_tac 1); by (Simp_tac 1); - by (SELECT_GOAL Safe_tac 1); - by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1); - by (Asm_full_simp_tac 1); by (Fast_tac 1); by (Asm_full_simp_tac 1); -by (rtac iffI 1); - by (eres_inst_tac [("x","bound_typ_inst S type_scheme1 -> bound_typ_inst S type_scheme2")] allE 1); - by (Asm_full_simp_tac 1); - by (Fast_tac 1); by (Fast_tac 1); qed "le_FVar"; Addsimps [le_FVar];