equal
deleted
inserted
replaced
67 (t, (TermC.mk_factroot op0 T fact (ni div (fact*fact))))) |
67 (t, (TermC.mk_factroot op0 T fact (ni div (fact*fact))))) |
68 end |
68 end |
69 | NONE => NONE) |
69 | NONE => NONE) |
70 | _ => NONE); |
70 | _ => NONE); |
71 |
71 |
72 (*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", str2term "sqrt 0"); |
72 (*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", TermC.parse_test @{context} "sqrt 0"); |
73 > eval_sqrt thmid op_ t thy; |
73 > eval_sqrt thmid op_ t thy; |
74 > val Free (n1,t1) = arg; |
74 > val Free (n1,t1) = arg; |
75 > val SOME ni = int_of_str n1; |
75 > val SOME ni = int_of_str n1; |
76 *) |
76 *) |
77 \<close> |
77 \<close> |