... |
... |
@@ -6,10 +6,13 @@ Source: git repository at https://github.com/jrh13/hol-light |
6
|
6
|
|
7
|
7
|
Files: *
|
8
|
8
|
Copyright: 1998 University of Cambridge
|
9
|
|
- 1998-2018 John Harrison <johnh@ichips.intel.com> and others
|
|
9
|
+ 1998-2024 John Harrison <johnh@ichips.intel.com> and others
|
10
|
10
|
2016-2017 Andrea Gabrielli
|
11
|
11
|
2015-2018 Marco Maggesi
|
12
|
12
|
2018 Michael Faerber
|
|
13
|
+ 2020 Mario Carneiro
|
|
14
|
+ 2000 Bruno Barras
|
|
15
|
+ 2024 Juneyoung Lee
|
13
|
16
|
License: BSD-2-clause
|
14
|
17
|
|
15
|
18
|
|
... |
... |
@@ -62,6 +65,7 @@ Comment: There is no license in subdirectory Unity, but Unity/README |
62
|
65
|
|
63
|
66
|
|
64
|
67
|
Files: RichterHilbertAxiomGeometry/*
|
|
68
|
+ Examples/inverse_bug*
|
65
|
69
|
Copyright: 2012, 2013 by Bill Richter
|
66
|
70
|
License: BSD-2-clause
|
67
|
71
|
Comment: There is no license in subdirectory
|
... |
... |
@@ -70,11 +74,14 @@ Comment: There is no license in subdirectory |
70
|
74
|
HOL Light.
|
71
|
75
|
|
72
|
76
|
|
73
|
|
-Files: RichterHilbertAxiomGeometry/from_topology.ml Multivariate/topology.ml
|
|
77
|
+Files: RichterHilbertAxiomGeometry/from_topology.ml Multivariate/*
|
74
|
78
|
Copyright: 1998-2017 John Harrison
|
75
|
79
|
2010 Valentina Bruno
|
76
|
80
|
2014-2017 Marco Maggesi
|
77
|
81
|
2016-2017 Andrea Gabrielli
|
|
82
|
+ 2008 Marco Maggesi, Graziano Gentili and Gianni Ciolli
|
|
83
|
+ 2007 Lars Schewe
|
|
84
|
+ 2011-2013 Sanaz Khan Afshar & Vincent Aravantinos
|
78
|
85
|
License: BSD-2-clause
|
79
|
86
|
Comment: There is no license in
|
80
|
87
|
RichterHilbertAxiomGeometry/from_topology.ml, but the file states
|
... |
... |
@@ -99,6 +106,9 @@ Comment: There is no license in subdirectory Functionspaces, but |
99
|
106
|
Functionspaces/README states that this directory is distributed under
|
100
|
107
|
the same license as HOL Light.
|
101
|
108
|
|
|
109
|
+Files: GL/*
|
|
110
|
+Copyright: 2020-2022 Marco Maggesi, Cosimo Perini Brogi
|
|
111
|
+License: BSD-2-clause
|
102
|
112
|
|
103
|
113
|
Files: IEEE/*
|
104
|
114
|
Copyright: 2014, Charlie Jacobsen, University of Utah
|
... |
... |
@@ -115,8 +125,11 @@ Copyright: 2009-2017, Petros Papapanagiotou, Jacques Fleuriot, |
115
|
125
|
License: BSD-2-clause
|
116
|
126
|
|
117
|
127
|
|
118
|
|
-Files: Library/q.ml
|
119
|
|
-Copyright: 2012-2013 Vincent Aravantinos, Hardware Verification Group,
|
|
128
|
+Files: Library/*
|
|
129
|
+Copyright: 2020 Mario Carneiro
|
|
130
|
+ 2019-2024 John Harrison
|
|
131
|
+ 2022-2024 June Lee
|
|
132
|
+ 2012-2013 Vincent Aravantinos, Hardware Verification Group,
|
120
|
133
|
Concordia University
|
121
|
134
|
License: BSD-2-clause
|
122
|
135
|
Comment: There is no license in Library/q.ml, but the file states that
|
... |
... |
@@ -152,9 +165,7 @@ Comment: There is no license in metis.ml, but the file states that |
152
|
165
|
it is distributed under the same license as HOL Light.
|
153
|
166
|
|
154
|
167
|
|
155
|
|
-Files: pa_j/pa_j_3.07.ml
|
156
|
|
- pa_j/pa_j_3.08.ml
|
157
|
|
- pa_j/pa_j_3.09.ml
|
|
168
|
+Files: pa_j/*
|
158
|
169
|
Copyright: 2002-2006 INRIA
|
159
|
170
|
1998-2017 John Harrison <johnh@ichips.intel.com> and others
|
160
|
171
|
License: LGPL-2
|