equal
deleted
inserted
replaced
31 variable. |
31 variable. |
32 Can you read diff_const in the Ouput window ? |
32 Can you read diff_const in the Ouput window ? |
33 |
33 |
34 Please, skip this introductory ML-section in the first go ...*} |
34 Please, skip this introductory ML-section in the first go ...*} |
35 ML {* |
35 ML {* |
36 default_print_depth 1; |
36 (*default_print_depth 1;*) |
37 val (thy, ro, er, inst) = |
37 val (thy, ro, er, inst) = |
38 (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
38 (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
39 *} |
39 *} |
40 text {* ... and let us differentiate the term t: *} |
40 text {* ... and let us differentiate the term t: *} |
41 ML {* |
41 ML {* |