equal
deleted
inserted
replaced
418 |
418 |
419 |
419 |
420 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------"; |
420 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------"; |
421 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------"; |
421 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------"; |
422 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------"; |
422 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------"; |
423 val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES")); |
423 val (op_, ef) = the (LibraryC.assoc (Know_Store.get_calcs @{theory}, "TIMES")); |
424 val t = TermC.parseNEW' ctxt "2 * (3::real)"; |
424 val t = TermC.parseNEW' ctxt "2 * (3::real)"; |
425 (*val SOME (thmid,t') = *)get_pair ctxt op_ ef t; |
425 (*val SOME (thmid,t') = *)get_pair ctxt op_ ef t; |
426 ; |
426 ; |
427 "~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) = |
427 "~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) = |
428 (thy, op_, ef, t); |
428 (thy, op_, ef, t); |