forked from immler/hol4isabelle
-
Notifications
You must be signed in to change notification settings - Fork 1
/
ROOT
134 lines (95 loc) · 2.47 KB
/
ROOT
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
(* Prekernel *)
session Prekernel in Prekernel = Pure +
theories
Prekernel
(* Original HOL4 Kernel *)
session Core_Original in Original = Prekernel +
theories
Core
session More_Original in "Original/More" = Core_Original +
theories
More
session Large_Original in "Original/Large" = More_Original +
theories
Large
session CakeML_Deps_Original in "Original/CakeML/Deps" = More_Original +
theories
CakeML_Deps
session CakeML_Semantics_Original in "Original/CakeML/Semantics" = CakeML_Deps_Original +
theories
CakeML_Semantics
session CakeML_Translator_Original in "Original/CakeML/Translator" = CakeML_Semantics_Original +
theories
CakeML_Translator
(* Isabelle/HOL HOL4 Kernel *)
session Core_Isabelle in Isabelle = HOL +
sessions
Prekernel
directories
"../splice"
theories
Core
session More_Isabelle in "Isabelle/More" = Core_Isabelle +
theories
More
session Large_Isabelle in "Isabelle/Large" = More_Isabelle +
theories
Large
session CakeML_Deps_Isabelle in "Isabelle/CakeML/Deps" = More_Isabelle +
theories
CakeML_Deps
session CakeML_Semantics_Isabelle in "Isabelle/CakeML/Semantics" = CakeML_Deps_Isabelle +
theories
CakeML_Semantics
session CakeML_Translator_Isabelle in "Isabelle/CakeML/Translator" = CakeML_Semantics_Isabelle +
theories
CakeML_Translator
(* Debug Kernel *)
session Core_Debug in Debug = Core_Isabelle +
sessions
Core_Original
theories
Core
session More_Debug in "Debug/More" = Core_Debug +
theories
More
session Large_Debug in "Debug/Large" = More_Debug +
theories
Large
(*
session HOL4_Core_Isabelle = HOL +
sessions
HOL4_Prekernel
theories
HOL4_Core_Isabelle
session HOL4_Core_Debug = HOL4_Core_Isabelle +
sessions
HOL4_Core_Original
theories
HOL4_Core_Debug
(* More *)
session HOL4_More_Isabelle = HOL4_Core_Isabelle +
theories
HOL4_More_Isabelle
session HOL4_More_Debug = HOL4_Core_Debug +
theories
HOL4_More_Debug
(* Large *)
session HOL4_Large_Isabelle = HOL4_More_Isabelle +
theories
HOL4_Large_Isabelle
session HOL4_Large_Debug = HOL4_More_Debug +
theories
HOL4_Large_Debug
(* CakeML semantics *)
session CakeML_Semantics_Isabelle = HOL4_Large_Isabelle +
theories
CakeML_Semantics_Isabelle
session CakeML_Semantics_Original = HOL4_Large_Original +
theories
CakeML_Semantics_Original
(* Example *)
session Example_Transfer = HOL4_Core_Isabelle +
theories
Example_Transfer
*)