equal
deleted
inserted
replaced
419 } |
419 } |
420 qed |
420 qed |
421 |
421 |
422 (* effect on printed locale *) |
422 (* effect on printed locale *) |
423 |
423 |
424 print_locale Rrgrp |
424 print_locale! Rrgrp |
425 print_locale Rlgrp |
425 print_locale! Rlgrp |
426 |
426 |
427 (* locale with many parameters --- |
427 (* locale with many parameters --- |
428 interpretations generate alternating group A5 *) |
428 interpretations generate alternating group A5 *) |
429 |
429 |
430 locale RA5 = var A + var B + var C + var D + var E + |
430 locale RA5 = var A + var B + var C + var D + var E + |