equal
deleted
inserted
replaced
25 |
25 |
26 final case class Header(val name: String, val imports: List[String], val uses: List[String]) |
26 final case class Header(val name: String, val imports: List[String], val uses: List[String]) |
27 } |
27 } |
28 |
28 |
29 |
29 |
30 class Thy_Header(symbols: Symbol.Interpretation) extends Outer_Parse.Parser |
30 class Thy_Header(symbols: Symbol.Interpretation) extends Parse.Parser |
31 { |
31 { |
32 import Thy_Header._ |
32 import Thy_Header._ |
33 |
33 |
34 |
34 |
35 /* header */ |
35 /* header */ |