equal
deleted
inserted
replaced
1600 "-------- fun eval_get_denominator -------------------------------------------"; |
1600 "-------- fun eval_get_denominator -------------------------------------------"; |
1601 "-------- fun eval_get_denominator -------------------------------------------"; |
1601 "-------- fun eval_get_denominator -------------------------------------------"; |
1602 val thy = @{theory Isac_Knowledge}; |
1602 val thy = @{theory Isac_Knowledge}; |
1603 val ctxt = Proof_Context.init_global thy; |
1603 val ctxt = Proof_Context.init_global thy; |
1604 val t = TermC.parseNEW' ctxt "get_denominator ((a +x)/b)"; |
1604 val t = TermC.parseNEW' ctxt "get_denominator ((a +x)/b)"; |
1605 val SOME (_, t') = eval_get_denominator "" 0 t thy; |
1605 val SOME (_, t') = eval_get_denominator "" 0 t ctxt; |
1606 if UnparseC.term t' = "get_denominator ((a + x) / b) = b" |
1606 if UnparseC.term t' = "get_denominator ((a + x) / b) = b" |
1607 then () else error "get_denominator ((a + x) / b) = b" |
1607 then () else error "get_denominator ((a + x) / b) = b" |
1608 |
1608 |
1609 |
1609 |
1610 "-------- several errpats in complicated term --------------------------------"; |
1610 "-------- several errpats in complicated term --------------------------------"; |