src/FOL/ex/LocaleTest.thy
changeset 17436 4e603046e539
parent 17228 19b460b39dad
child 19783 82f365a14960
equal deleted inserted replaced
17435:0eed5a1c00c1 17436:4e603046e539
   134 print_interps ID  (* output: i2 *)
   134 print_interps ID  (* output: i2 *)
   135 
   135 
   136 
   136 
   137 interpretation i3: ID [X "Y::i"] .
   137 interpretation i3: ID [X "Y::i"] .
   138 
   138 
   139 (* duplicate: not registered *)
   139 (* duplicate: thm not added *)
   140 
   140 
   141 (* thm i3.a.asm_A *)
   141 (* thm i3.a.asm_A *)
   142 
   142 
   143 
   143 
   144 print_interps IA  (* output: <no prefix>, i1 *)
   144 print_interps IA  (* output: <no prefix>, i1 *)