equal
deleted
inserted
replaced
1907 (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) |
1907 (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) |
1908 (Bound 2))))))))" |
1908 (Bound 2))))))))" |
1909 |
1909 |
1910 ML {* @{code cooper_test} () *} |
1910 ML {* @{code cooper_test} () *} |
1911 |
1911 |
1912 (* |
1912 code_reflect |
1913 code_reserved SML oo |
1913 functions pa |
1914 export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML" |
1914 module_name Generated_Cooper |
1915 *) |
1915 file "~~/src/HOL/Tools/Qelim/generated_cooper.ML" |
1916 |
1916 |
1917 oracle linzqe_oracle = {* |
1917 oracle linzqe_oracle = {* |
1918 let |
1918 let |
1919 |
1919 |
1920 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t |
1920 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t |