equal
deleted
inserted
replaced
2035 |
2035 |
2036 section "Implement floatarith" |
2036 section "Implement floatarith" |
2037 |
2037 |
2038 subsection "Define syntax and semantics" |
2038 subsection "Define syntax and semantics" |
2039 |
2039 |
2040 datatype floatarith |
2040 datatype_new floatarith |
2041 = Add floatarith floatarith |
2041 = Add floatarith floatarith |
2042 | Minus floatarith |
2042 | Minus floatarith |
2043 | Mult floatarith floatarith |
2043 | Mult floatarith floatarith |
2044 | Inverse floatarith |
2044 | Inverse floatarith |
2045 | Cos floatarith |
2045 | Cos floatarith |
2454 case (Var n) |
2454 case (Var n) |
2455 from this[symmetric] `bounded_by xs vs`[THEN bounded_byE, of n] |
2455 from this[symmetric] `bounded_by xs vs`[THEN bounded_byE, of n] |
2456 show ?case by (cases "n < length vs", auto) |
2456 show ?case by (cases "n < length vs", auto) |
2457 qed |
2457 qed |
2458 |
2458 |
2459 datatype form = Bound floatarith floatarith floatarith form |
2459 datatype_new form = Bound floatarith floatarith floatarith form |
2460 | Assign floatarith floatarith form |
2460 | Assign floatarith floatarith form |
2461 | Less floatarith floatarith |
2461 | Less floatarith floatarith |
2462 | LessEqual floatarith floatarith |
2462 | LessEqual floatarith floatarith |
2463 | AtLeastAtMost floatarith floatarith floatarith |
2463 | AtLeastAtMost floatarith floatarith floatarith |
2464 |
2464 |