equal
deleted
inserted
replaced
456 else |
456 else |
457 raise exn |
457 raise exn |
458 end |
458 end |
459 | _ => raise exn |
459 | _ => raise exn |
460 ) |
460 ) |
461 val th = ref ([]: Theory.theory list) |
461 val th = ref ([]: theory list) |
462 val sg = ref ([]: Sign.sg list) |
462 val sg = ref ([]: Sign.sg list) |
463 |
463 |
464 fun invoke_float_op c = |
464 fun invoke_float_op c = |
465 let |
465 let |
466 val th = (if length(!th) = 0 then th := [theory "MatrixLP"] else (); hd (!th)) |
466 val th = (if length(!th) = 0 then th := [theory "MatrixLP"] else (); hd (!th)) |