equal
deleted
inserted
replaced
27 add_SI1m : "((a SI1m) + (b SI1m)) = ((a + b) SI1m)" and |
27 add_SI1m : "((a SI1m) + (b SI1m)) = ((a + b) SI1m)" and |
28 add_SI1cm : "((a SI1cm) + (b SI1cm)) = ((a + b) SI1cm)" |
28 add_SI1cm : "((a SI1cm) + (b SI1cm)) = ((a + b) SI1cm)" |
29 |
29 |
30 ML \<open> |
30 ML \<open> |
31 Thm.prop_of @{thm SI1m__cm}; |
31 Thm.prop_of @{thm SI1m__cm}; |
32 TermC.atomt (Thm.prop_of @{thm SI1m__cm}); |
32 TermC.atom_trace @{context} (Thm.prop_of @{thm SI1m__cm}); |
33 \<close> |
33 \<close> |
34 |
34 |
35 (*--------------------- broken Isabelle2015->17 ------------- |
35 (*--------------------- broken Isabelle2015->17 ------------- |
36 theorem ad_hoc_1: "((2 SI1m) * 3) = (600 SI1cm)" |
36 theorem ad_hoc_1: "((2 SI1m) * 3) = (600 SI1cm)" |
37 proof - |
37 proof - |