changeset 36798 | 3981db162131 |
parent 36608 | 16736dde54c0 |
child 37887 | 2ae085b07f2f |
36797:cb074cec7a30 | 36798:3981db162131 |
---|---|
1908 (Bound 2))))))))" |
1908 (Bound 2))))))))" |
1909 |
1909 |
1910 ML {* @{code cooper_test} () *} |
1910 ML {* @{code cooper_test} () *} |
1911 |
1911 |
1912 (* |
1912 (* |
1913 code_reflect Generated_Cooper |
1913 code_reflect Cooper_Procedure |
1914 functions pa |
1914 functions pa |
1915 file "~~/src/HOL/Tools/Qelim/generated_cooper.ML" |
1915 file "~~/src/HOL/Tools/Qelim/generated_cooper.ML" |
1916 *) |
1916 *) |
1917 |
1917 |
1918 oracle linzqe_oracle = {* |
1918 oracle linzqe_oracle = {* |