Summary
- hiding internal construction of partial_function_mr, ML-interface returns simp-thms
The file was modified | thys/Partial_Function_MR/Partial_Function_MR_Examples.thy (diff) |
The file was modified | thys/Partial_Function_MR/partial_function_mr.ML (diff) |