equal
deleted
inserted
replaced
15 (*Script-names*) |
15 (*Script-names*) |
16 Solve'_log :: "[bool,real, bool list] |
16 Solve'_log :: "[bool,real, bool list] |
17 => bool list" |
17 => bool list" |
18 ("((Script Solve'_log (_ _=))//(_))" 9) |
18 ("((Script Solve'_log (_ _=))//(_))" 9) |
19 |
19 |
20 rules |
20 axioms |
21 |
21 |
22 equality_pow "0 < a ==> (l = r) = (a^^^l = a^^^r)" |
22 equality_pow: "0 < a ==> (l = r) = (a^^^l = a^^^r)" |
23 (* this is what students ^^^^^^^... are told to do *) |
23 (* this is what students ^^^^^^^... are told to do *) |
24 equality_power "((a log b) = c) = (a^^^(a log b) = a^^^c)" |
24 equality_power: "((a log b) = c) = (a^^^(a log b) = a^^^c)" |
25 exp_invers_log "a^^^(a log b) = b" |
25 exp_invers_log: "a^^^(a log b) = b" |
26 |
26 |
27 ML {* |
27 ML {* |
28 val thy = @{theory}; |
28 val thy = @{theory}; |
29 |
29 |
30 (** problems **) |
30 (** problems **) |