equal
deleted
inserted
replaced
1869 (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) |
1869 (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) |
1870 (Bound 2))))))))" |
1870 (Bound 2))))))))" |
1871 |
1871 |
1872 ML {* @{code cooper_test} () *} |
1872 ML {* @{code cooper_test} () *} |
1873 |
1873 |
1874 (* |
1874 (* code_reflect Cooper_Procedure |
1875 code_reflect Cooper_Procedure |
|
1876 functions pa |
1875 functions pa |
1877 file "~~/src/HOL/Tools/Qelim/generated_cooper.ML" |
1876 file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML" *) |
1878 *) |
|
1879 |
1877 |
1880 oracle linzqe_oracle = {* |
1878 oracle linzqe_oracle = {* |
1881 let |
1879 let |
1882 |
1880 |
1883 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t |
1881 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t |