Skip to content
Success

Changes

Summary

  1. getting rid of "nonempty_witness"
Changeset 6525:a647bfff9a77 by paulson _lp15@cam.ac.uk_:
getting rid of "nonempty_witness"
The file was modified thys/Echelon_Form/Rings2.thy (diff)
The file was modified thys/QR_Decomposition/Gram_Schmidt_IArrays.thy (diff)
The file was modified thys/pGCL/LoopInduction.thy (diff)
The file was modified thys/pGCL/Misc.thy (diff)
The file was modified thys/pGCL/WellDefined.thy (diff)