equal
deleted
inserted
replaced
1934 "cooper_test u = pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1))) |
1934 "cooper_test u = pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1))) |
1935 (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) |
1935 (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) |
1936 (Bound 2))))))))" |
1936 (Bound 2))))))))" |
1937 |
1937 |
1938 code_reserved SML oo |
1938 code_reserved SML oo |
1939 code_gen pa cooper_test in SML to GeneratedCooper |
1939 code_gen pa cooper_test in SML module_name GeneratedCooper |
1940 (*code_gen pa in SML to GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*) |
1940 (*code_gen pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*) |
1941 |
1941 |
1942 ML {* GeneratedCooper.cooper_test () *} |
1942 ML {* GeneratedCooper.cooper_test () *} |
1943 use "coopereif.ML" |
1943 use "coopereif.ML" |
1944 oracle linzqe_oracle ("term") = Coopereif.cooper_oracle |
1944 oracle linzqe_oracle ("term") = Coopereif.cooper_oracle |
1945 use "coopertac.ML" |
1945 use "coopertac.ML" |