equal
deleted
inserted
replaced
9 |
9 |
10 LOGICS="HOL ZF" |
10 LOGICS="HOL ZF" |
11 DISTBASE=~/tmp/isadist |
11 DISTBASE=~/tmp/isadist |
12 ROOT=/usr/share |
12 ROOT=/usr/share |
13 BIN=/usr/bin |
13 BIN=/usr/bin |
14 RPMRELEASE=1 |
14 RPMRELEASE=2 |
15 |
15 |
16 |
16 |
17 ## diagnostics |
17 ## diagnostics |
18 |
18 |
19 PRG=$(basename $0) |
19 PRG=$(basename $0) |
113 |
113 |
114 %description |
114 %description |
115 |
115 |
116 This package contains the full source distribution of Isabelle |
116 This package contains the full source distribution of Isabelle |
117 together with documentation. To make it actually run you still need |
117 together with documentation. To make it actually run you still need |
118 the SML/NJ 110 compiler and any of the precompiled Isabelle |
118 the ML compiler and any of the precompiled Isabelle object-logics |
119 object-logics (e.g. package isabelle-HOL). |
119 (e.g. package isabelle-HOL). |
120 |
120 |
121 |
121 |
122 Isabelle is a popular generic theorem proving environment developed at |
122 Isabelle is a popular generic theorem proving environment developed at |
123 Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow). |
123 Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow). |
124 The system can be viewed from two main perspectives. On the one hand |
124 The system can be viewed from two main perspectives. On the one hand |