summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/LCF/LCF.thy

changeset 17249 | e89fbfd778c1 |

parent 17248 | 81bf91654e73 |

child 19757 | 4a2a71c31968 |

equal
deleted
inserted
replaced

17248:81bf91654e73 | 17249:e89fbfd778c1 |
---|---|

6 |
6 |

7 header {* LCF on top of First-Order Logic *} |
7 header {* LCF on top of First-Order Logic *} |

8 |
8 |

9 theory LCF |
9 theory LCF |

10 imports FOL |
10 imports FOL |

11 uses ("pair.ML") ("fix.ML") |
11 uses ("LCF_lemmas.ML") ("pair.ML") ("fix.ML") |

12 begin |
12 begin |

13 |
13 |

14 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *} |
14 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *} |

15 |
15 |

16 subsection {* Natural Deduction Rules for LCF *} |
16 subsection {* Natural Deduction Rules for LCF *} |