src/FOL/ex/LocaleTest.thy
changeset 27761 b95e9ba0ca1d
parent 27718 3a85bc6bfd73
child 28085 914183e229e9
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Wed Aug 06 13:57:25 2008 +0200
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Wed Aug 06 16:41:40 2008 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4  
     1.5  (* without prefix *)
     1.6  
     1.7 -interpretation IC ["W::i" "Z::i"] .  (* subsumed by i1: IC *)
     1.8 +interpretation IC ["W::i" "Z::i"] by intro_locales  (* subsumed by i1: IC *)
     1.9  interpretation IC ["W::'a" "Z::i"] by unfold_locales auto
    1.10    (* subsumes i1: IA and i1: IC *)
    1.11  
    1.12 @@ -151,7 +151,7 @@
    1.13  print_interps ID  (* output: i2, i3 *)
    1.14  
    1.15  
    1.16 -interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] .
    1.17 +interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] by intro_locales
    1.18  
    1.19  corollary (in ID) th_x: True ..
    1.20  
    1.21 @@ -184,7 +184,7 @@
    1.22  proof -
    1.23    fix alpha::i and beta
    1.24    have alpha_A: "IA(alpha)" by unfold_locales
    1.25 -  interpret i5: IA [alpha] .  (* subsumed *)
    1.26 +  interpret i5: IA [alpha] by intro_locales  (* subsumed *)
    1.27    print_interps IA  (* output: <no prefix>, i1 *)
    1.28    interpret i6: IC [alpha beta] by unfold_locales auto
    1.29    print_interps IA   (* output: <no prefix>, i1 *)