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

src/HOL/ROOT

changeset 48458 | 09710d6fc3d1 |

parent 48421 | c4d337782de4 |

child 48470 | 7483aa690b4f |

equal
deleted
inserted
replaced

48457:fd9e28d5a143 | 48458:09710d6fc3d1 |
---|---|

4 theories Complex_Main |
4 theories Complex_Main |

5 files "document/root.tex" "document/root.bib" |
5 files "document/root.tex" "document/root.bib" |

6 |
6 |

7 session "HOL-Base"! in "." = Pure + |
7 session "HOL-Base"! in "." = Pure + |

8 description {* Raw HOL base, with minimal tools *} |
8 description {* Raw HOL base, with minimal tools *} |

9 options [document = false] |
9 options [no_document] |

10 theories HOL |
10 theories HOL |

11 |
11 |

12 session "HOL-Plain"! in "." = Pure + |
12 session "HOL-Plain"! in "." = Pure + |

13 description {* HOL side-entry after bootstrap of many tools and packages *} |
13 description {* HOL side-entry after bootstrap of many tools and packages *} |

14 options [document = false] |
14 options [no_document] |

15 theories Plain |
15 theories Plain |

16 |
16 |

17 session "HOL-Main"! in "." = Pure + |
17 session "HOL-Main"! in "." = Pure + |

18 description {* HOL side-entry for Main only, without Complex_Main *} |
18 description {* HOL side-entry for Main only, without Complex_Main *} |

19 options [document = false] |
19 options [no_document] |

20 theories Main |
20 theories Main |

21 |
21 |

22 session "HOL-Proofs"! (2) in "." = Pure + |
22 session "HOL-Proofs"! (2) in "." = Pure + |

23 description {* HOL-Main with proof terms *} |
23 description {* HOL-Main with proof terms *} |

24 options [document = false, proofs = 2, parallel_proofs = 0] |
24 options [no_document, proofs = 2, parallel_proofs = 0] |

25 theories Main |
25 theories Main |

26 |
26 |

27 session HOLCF! (3) = HOL + |
27 session HOLCF! (3) = HOL + |

28 description {* |
28 description {* |

29 Author: Franz Regensburger |
29 Author: Franz Regensburger |

30 Author: Brian Huffman |
30 Author: Brian Huffman |

31 |
31 |

32 HOLCF -- a semantic extension of HOL by the LCF logic. |
32 HOLCF -- a semantic extension of HOL by the LCF logic. |

33 *} |
33 *} |

34 options [document_graph] |
34 options [document_graph] |

35 theories [document = false] |
35 theories [no_document] |

36 "~~/src/HOL/Library/Nat_Bijection" |
36 "~~/src/HOL/Library/Nat_Bijection" |

37 "~~/src/HOL/Library/Countable" |
37 "~~/src/HOL/Library/Countable" |

38 theories Plain_HOLCF Fixrec HOLCF |
38 theories Plain_HOLCF Fixrec HOLCF |

39 files "document/root.tex" |
39 files "document/root.tex" |

40 |
40 |