equal
deleted
inserted
replaced
97 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct); |
97 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct); |
98 val ct = "d_d x 2"; |
98 val ct = "d_d x 2"; |
99 val SOME (ctt,_) = |
99 val SOME (ctt,_) = |
100 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct); |
100 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct); |
101 "----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----"; |
101 "----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----"; |
102 trace_rewrite := true; |
102 trace_rewrite := false; |
103 val ct = "d_d s a"; |
103 val ct = "d_d s a"; |
104 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct); |
104 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct); |
105 (*got: NONE instead SOME*) |
105 (*got: NONE instead SOME*) |
106 eval_true (@{theory "Isac"}) [str2term "a is_const"] (assoc_rls"erls"); |
106 eval_true (@{theory "Isac"}) [str2term "a is_const"] (assoc_rls"erls"); |
107 (*got: false instead true; ~~~~~~~~~~~ replaced by 'is_atom'*) |
107 (*got: false instead true; ~~~~~~~~~~~ replaced by 'is_atom'*) |