| branch | isac-update-Isa09-2 |
| changeset 38014 | 3e11e3c2dc42 |
| parent 37960 | ec20007095f2 |
| 38013:e4f42a63d665 | 38014:3e11e3c2dc42 |
|---|---|
36 |
36 |
37 |
37 |
38 val thy = Float.thy; |
38 val thy = Float.thy; |
39 |
39 |
40 (*.calculate the value of a pair of floats.*) |
40 (*.calculate the value of a pair of floats.*) |
41 val ((a,b),(c,d)) = calc "op +" ((~1,0),(0,0)) ((2,0),(0,0)); |
41 val ((a,b),(c,d)) = calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0)); |
42 |
42 |
43 |
43 |
44 (*.build the term.*) |
44 (*.build the term.*) |
45 term_of_float HOLogic.realT ((~1,0),(0,0)); |
45 term_of_float HOLogic.realT ((~1,0),(0,0)); |
46 term_of_float HOLogic.realT ((~1,11),(0,0)); |
46 term_of_float HOLogic.realT ((~1,11),(0,0)); |
111 (*--18.3.05-------------------------*) |
111 (*--18.3.05-------------------------*) |
112 |
112 |
113 |
113 |
114 (*.the function evaluating a binary operator.*) |
114 (*.the function evaluating a binary operator.*) |
115 val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))"; |
115 val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))"; |
116 val SOME (thmid, t) = eval_binop "#add_" "op +" t thy; |
116 val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" t thy; |
117 term2str t; |
117 term2str t; |
118 |
118 |
119 |
119 |
120 (*.scan a term for a pair of floats.*) |
120 (*.scan a term for a pair of floats.*) |
121 val SOME (thmid,t') = get_pair thy op_ eval_fn t; |
121 val SOME (thmid,t') = get_pair thy op_ eval_fn t; |