src/FOL/ex/LocaleTest.thy
 changeset 33617 bfee47887ca3 parent 33462 ddcf2004e215 child 33671 4b0f2599ed48 child 33835 d6134fb5a49f
equal inserted replaced
33616:69f0a6271825 33617:bfee47887ca3
`   451   (* the latter comes through the sublocale relation *)`
`   451   (* the latter comes through the sublocale relation *)`
`   452 `
`   452 `
`   453 `
`   453 `
`   454 subsection {* Interpretation in theory, then sublocale *}`
`   454 subsection {* Interpretation in theory, then sublocale *}`
`   455 `
`   455 `
`   456 interpretation (* fol: *) logic "op +" "minus"`
`   456 interpretation fol: logic "op +" "minus"`
`   457 (* FIXME declaration of qualified names *)`
`       `
`   458   by unfold_locales (rule int_assoc int_minus2)+`
`   457   by unfold_locales (rule int_assoc int_minus2)+`
`   459 `
`   458 `
`   460 locale logic2 =`
`   459 locale logic2 =`
`   461   fixes land (infixl "&&" 55)`
`   460   fixes land (infixl "&&" 55)`
`   462     and lnot ("-- _"  60)`
`   461     and lnot ("-- _"  60)`
`   463   assumes assoc: "(x && y) && z = x && (y && z)"`
`   462   assumes assoc: "(x && y) && z = x && (y && z)"`
`   464     and notnot: "-- (-- x) = x"`
`   463     and notnot: "-- (-- x) = x"`
`   465 begin`
`   464 begin`
`   466 `
`   465 `
`   468 definition lor (infixl "||" 50) where`
`   466 definition lor (infixl "||" 50) where`
`   469   "x || y = --(-- x && -- y)"`
`   467   "x || y = --(-- x && -- y)"`
`   471 `
`   468 `
`   472 end`
`   469 end`
`   473 `
`   470 `
`   474 sublocale logic < two: logic2`
`   471 sublocale logic < two: logic2`
`   475   by unfold_locales (rule assoc notnot)+`
`   472   by unfold_locales (rule assoc notnot)+`
`   476 `
`   473 `
`   477 thm two.assoc`
`   474 thm fol.two.assoc`
`   478 `
`   475 `
`   479 `
`   476 `
`   480 subsection {* Declarations and sublocale *}`
`   477 subsection {* Declarations and sublocale *}`
`   481 `
`   478 `
`   482 locale logic_a = logic`
`   479 locale logic_a = logic`