Skip to content
Success

Changes

Summary

  1. hiding internal construction of partial_function_mr, ML-interface returns simp-thms
Changeset 8304:f4af77165abd by rene thiemann _rene.thiemann@uibk.ac.at_:
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)