Summary
- hide internal construction of partial_function_mr
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) |
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) |