equal
deleted
inserted
replaced
5789 ML {* @{code test2} () *} |
5789 ML {* @{code test2} () *} |
5790 ML {* @{code test3} () *} |
5790 ML {* @{code test3} () *} |
5791 ML {* @{code test4} () *} |
5791 ML {* @{code test4} () *} |
5792 ML {* @{code test5} () *} |
5792 ML {* @{code test5} () *} |
5793 |
5793 |
5794 (*export_code mircfrqe mirlfrqe |
5794 (*code_reflect |
5795 in SML module_name Mir file "raw_mir.ML"*) |
5795 functions mircfrqe mirlfrqe |
|
5796 module_name Mir |
|
5797 file "mir.ML"*) |
5796 |
5798 |
5797 oracle mirfr_oracle = {* fn (proofs, ct) => |
5799 oracle mirfr_oracle = {* fn (proofs, ct) => |
5798 let |
5800 let |
5799 |
5801 |
5800 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t |
5802 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t |