summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Pure/Proof/ROOT.ML

author | berghofe |

Thu Apr 21 19:12:03 2005 +0200 (2005-04-21) | |

changeset 15797 | a63605582573 |

parent 14981 | e73f8140af78 |

permissions | -rw-r--r-- |

- Eliminated nodup_vars check.

- Unification and matching functions now check types of term variables / sorts

of type variables when applying a substitution.

- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list

as argument, to allow for proper instantiation of theorems containing

type variables with same name but different sorts.

- Unification and matching functions now check types of term variables / sorts

of type variables when applying a substitution.

- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list

as argument, to allow for proper instantiation of theorems containing

type variables with same name but different sorts.