1122 *** ------------- |
1122 *** ------------- |
1123 *** Const ( op =, [RealDef.real, RealDef.real] => bool) |
1123 *** Const ( op =, [RealDef.real, RealDef.real] => bool) |
1124 *** Free ( R, RealDef.real) |
1124 *** Free ( R, RealDef.real) |
1125 *** Free ( R, RealDef.real) *) |
1125 *** Free ( R, RealDef.real) *) |
1126 |
1126 |
|
1127 (*fun parse_patt thy str = |
|
1128 (**** prep_pbt: syntax error in '#Where' of ["equation"] |
|
1129 *** Exception- TOPLEVEL_ERROR raised |
|
1130 *** At command "ML" (line 172 of "/usr/local/isabisac/src/Tools/isac/Knowledge/Poly.thy").*) |
|
1131 (typ_a2real o numbers_to_string o |
|
1132 ProofContext.read_term_pattern (thy2ctxt thy)) str;*) |
1127 fun parse_patt thy str = |
1133 fun parse_patt thy str = |
1128 ProofContext.read_term_pattern (thy2ctxt thy) str; |
1134 ProofContext.read_term_pattern (thy2ctxt thy) str; |
|
1135 (*fun parse_patt thy str = (thy, str) |>> thy2ctxt |
|
1136 |-> ProofContext.read_term_pattern |
|
1137 |> numbers_to_string |
|
1138 |> typ_a2real;*) |
1129 |
1139 |
1130 (*version for testing local to theories*) |
1140 (*version for testing local to theories*) |
1131 fun str2term_ thy str = (term_of o the o (parse thy)) str; |
1141 fun str2term_ thy str = (term_of o the o (parse thy)) str; |
1132 fun str2term str = (term_of o the o (parse (theory "Isac"))) str; |
1142 fun str2term str = (term_of o the o (parse (theory "Isac"))) str; |
1133 fun strs2terms ss = map str2term ss; |
1143 fun strs2terms ss = map str2term ss; |