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

src/FOLP/ROOT.ML

author | wenzelm |

Sun Sep 18 14:25:48 2005 +0200 (2005-09-18) | |

changeset 17480 | fd19f77dcf60 |

parent 6349 | f7750d816c21 |

child 25750 | 4e796867ccb5 |

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

converted to Isar theory format;

1 (* Title: FOLP/ROOT.ML

2 ID: $Id$

3 Author: martin Coen, Cambridge University Computer Laboratory

4 Copyright 1993 University of Cambridge

6 Modifed version of Lawrence Paulson's FOL that contains proof terms.

8 Presence of unknown proof term means that matching does not behave as expected.

9 *)

11 val banner = "First-Order Logic with Natural Deduction with Proof Terms";

12 writeln banner;

14 use_thy "FOLP";