equal
deleted
inserted
replaced
8 Note: Isabelle/ML is the primary environment for logical operations. |
8 Note: Isabelle/ML is the primary environment for logical operations. |
9 */ |
9 */ |
10 |
10 |
11 package isac.gui.mawen.syntax.isabelle |
11 package isac.gui.mawen.syntax.isabelle |
12 |
12 |
13 import info.hupel.isabelle.pure._ |
13 import edu.tum.cs.isabelle.pure._ |
14 |
14 |
15 object XTerm |
15 object XTerm |
16 { |
16 { |
17 /* //---------- this would overwrite info.hupel.isabelle.pure._ ----------\\ |
17 /* //---------- this would overwrite edu.tum.cs.isabelle.pure._ ----------\\ |
18 |
18 |
19 type Indexname = (String, Int) |
19 type Indexname = (String, Int) |
20 |
20 |
21 type Sort = List[String] |
21 type Sort = List[String] |
22 val dummyS: Sort = List("") |
22 val dummyS: Sort = List("") |
33 case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
33 case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
34 case class Bound(index: Int) extends Term |
34 case class Bound(index: Int) extends Term |
35 case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term |
35 case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term |
36 case class App(fun: Term, arg: Term) extends Term |
36 case class App(fun: Term, arg: Term) extends Term |
37 |
37 |
38 \\---------- this would overwrite info.hupel.isabelle.pure._ ----------// */ |
38 \\---------- this would overwrite edu.tum.cs.isabelle.pure._ ----------// */ |
39 |
39 |
40 //----------------- ADDITIONS TO Isabelle2016-1 FOR ISAC -----------------\\ |
40 //----------------- ADDITIONS TO Isabelle2016-1 FOR ISAC -----------------\\ |
41 // see ~~/src/Pure/General/symbol.scala: is digit |
41 // see ~~/src/Pure/General/symbol.scala: is digit |
42 def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9' |
42 def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9' |
43 |
43 |