equal
deleted
inserted
replaced
78 *} |
78 *} |
79 ML {* |
79 ML {* |
80 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty); |
80 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty); |
81 Envir.subst_term subst (*pres?*); |
81 Envir.subst_term subst (*pres?*); |
82 *} |
82 *} |
83 ML {*print_depth 5*} |
|
84 use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*) |
83 use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*) |
85 |
84 ML {* |
86 ML {*theory "Isac"; |
85 the o (parse thy); |
87 theory "Poly"; |
86 ((parse thy)) "9 = 3 ^^^ 2"; |
88 theory "Rational"; |
87 (the o (parse thy)) "9 = 3 ^^^ 2"; |
89 theory "Equation"; |
88 (term_of o the o (parse thy)) "9 = 3 ^^^ 2"; |
|
89 Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2"; |
|
90 cterm_of (theory "Isac") (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2"); |
|
91 (make_thm o (cterm_of (theory "Isac"))) |
|
92 (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2"); |
90 *} |
93 *} |
91 |
94 |
92 ML {*theory "Isac"; |
95 ML {* |
93 assoc_thy; |
96 str2term "1 < (2 :: real)"; |
94 cancel; |
|
95 assoc_thy "Poly"; |
|
96 assoc_thy "Rational"; |
|
97 assoc_thy "Equation"; |
|
98 *} |
97 *} |
99 |
98 |
100 use"../../../test/Tools/isac/Knowledge/rational.sml" |
99 use"../../../test/Tools/isac/Knowledge/rational.sml" |
|
100 |
|
101 ML {*111*} |
|
102 |
101 (* |
103 (* |
102 use"equation.sml"; |
104 use"equation.sml"; |
103 use"root.sml"; |
105 use"root.sml"; |
104 (*use"inssort.sml"; problems with recdef in Isabelle2002*) |
106 (*use"inssort.sml"; problems with recdef in Isabelle2002*) |
105 use"rooteq.sml"; |
107 use"rooteq.sml"; |