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

doc-src/Logics/abstract.txt

author | haftmann |

Wed Dec 27 19:10:06 2006 +0100 (2006-12-27) | |

changeset 21915 | 4e63c55f4cb4 |

parent 104 | d8205bb279a7 |

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

different handling of type variable names

1 Isabelle's Object-Logics. Report 286.

3 This is the third of the Isabelle manuals. It covers Isabelle's built-in

4 object logics: first-order logic (FOL), Zermelo-Fraenkel set theory (ZF),

5 higher-order logic (HOL), the classical sequent calculus (LK), and

6 constructive type theory (CTT). The final chapter discusses how to define

7 new logics. This manual assumes familiarity with Report 280, Introduction

8 to Isabelle.