equal
deleted
inserted
replaced
399 apply (simp add: relcl_def) |
399 apply (simp add: relcl_def) |
400 done |
400 done |
401 |
401 |
402 theorem relcl_latticeof_eq: |
402 theorem relcl_latticeof_eq: |
403 "[|refl UNIV r; trans r|] ==> relcl (latticeof r) = r" |
403 "[|refl UNIV r; trans r|] ==> relcl (latticeof r) = r" |
404 by (simp add: relcl_def cl_latticeof, blast) |
404 by (simp add: relcl_def cl_latticeof) |
405 |
405 |
406 |
406 |
407 subsubsection {*Decoupling Theorems*} |
407 subsubsection {*Decoupling Theorems*} |
408 |
408 |
409 constdefs |
409 constdefs |