src/FOL/ex/LocaleTest.thy
changeset 15624 484178635bd8
parent 15598 4ab52355bb53
child 15696 1da4ce092c0b
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Thu Mar 24 16:36:40 2005 +0100
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Thu Mar 24 17:03:37 2005 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  print_interps L
     1.5  print_interps M
     1.6  
     1.7 -interpretation test [simp]: L .
     1.8 +interpretation test [simp]: L print_interps M .
     1.9  
    1.10  interpretation L .
    1.11  
    1.12 @@ -52,8 +52,19 @@
    1.13  
    1.14  print_interps A
    1.15  
    1.16 -(*
    1.17 -thm asm_A a.asm_A p1.a.asm_A
    1.18 +(* possible accesses
    1.19 +thm p1.a.asm_A thm LocaleTest.p1.a.asm_A
    1.20 +thm LocaleTest.asm_A thm p1.asm_A
    1.21 +*)
    1.22 +
    1.23 +(* without prefix *)
    1.24 +
    1.25 +interpretation C ["W::'b" "Z::'b"] by (auto intro: A.intro C_axioms.intro)
    1.26 +
    1.27 +print_interps A
    1.28 +
    1.29 +(* possible accesses
    1.30 +thm a.asm_A thm asm_A thm LocaleTest.a.asm_A thm LocaleTest.asm_A
    1.31  *)
    1.32  
    1.33  interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute)
    1.34 @@ -64,7 +75,7 @@
    1.35  thm p2.a.asm_A
    1.36  *)
    1.37  
    1.38 -interpretation p3: D [X Y] by (auto intro: A.intro)
    1.39 +interpretation p3: D [X Y] .
    1.40  
    1.41  (* duplicate: not registered *)
    1.42  (*
    1.43 @@ -87,4 +98,18 @@
    1.44  interpretation A [Z] apply - apply (auto intro: A.intro) done
    1.45  *)
    1.46  
    1.47 +theorem True
    1.48 +proof -
    1.49 +  fix alpha::i and beta::i and gamma::i
    1.50 +  assume "A(alpha)"
    1.51 +  then interpret p5: A [alpha] .
    1.52 +  print_interps A
    1.53 +  interpret p6: C [alpha beta] by (auto intro: C_axioms.intro)
    1.54 +  print_interps A   (* p6 not added! *)
    1.55 +  print_interps C
    1.56 +qed rule
    1.57 +
    1.58 +(* lemma "bla.bla": True by rule *)
    1.59 +
    1.60 +
    1.61  end