equal
deleted
inserted
replaced
2 use"wn.sml"; |
2 use"wn.sml"; |
3 |
3 |
4 various test dependent on IsacKnowledge/ outside Test.thy, Test.ML*) |
4 various test dependent on IsacKnowledge/ outside Test.thy, Test.ML*) |
5 |
5 |
6 |
6 |
7 val t = TermC.str2term "solve (a*x + b = c, x)"; |
7 val t = TermC.parse_test @{context} "solve (a*x + b = c, x)"; |
8 TermC.atomty t; |
8 TermC.atomty t; |
9 (* |
9 (* |
10 "\n*** -------------" |
10 "\n*** -------------" |
11 "\n*** Const ( Equation.solve, bool * real => bool list)" |
11 "\n*** Const ( Equation.solve, bool * real => bool list)" |
12 ... ~~~~~ ~~~~~~~~*) |
12 ... ~~~~~ ~~~~~~~~*) |