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

src/Pure/README

author | berghofe |

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

changeset 15797 | a63605582573 |

parent 6127 | ece970eb5850 |

child 16115 | ae921f717a2b |

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.

2 Pure: The Pure Isabelle System

5 This directory contains the ML source files for Pure Isabelle, which

6 is the basis for all object-logics:

8 IsaMakefile compiles the Pure system (use isatool make)

9 ML-Systems/ compatibility files for various ML systems

10 General/ general tools

11 Syntax/ the syntax module

12 Thy/ the theory file parser (old format) and loader

13 Isar/ Intelligible Semi-Automated Reasoning subsystem

14 ./ the actual meta logic implementation (see ROOT.ML)

16 Isabelle programmers may want to have a look at the generic modules

17 Library (see library.ML) and those in General/ (see General/README).