src/FOL/ex/NewLocaleTest.thy
changeset 28936 f1647bf418f5
parent 28927 7e631979922f
child 28993 829e684b02ef
equal deleted inserted replaced
28927:7e631979922f 28936:f1647bf418f5
   155   }
   155   }
   156   note x = this
   156   note x = this
   157   show ?t by (rule x [OF `?a`])
   157   show ?t by (rule x [OF `?a`])
   158 qed
   158 qed
   159 
   159 
   160 lemma
       
   161   assumes "P <-> P" (is "?p <-> _")
       
   162   shows "?p <-> ?p"
       
   163   .
       
   164 
       
   165 
   160 
   166 text {* Interpretation between locales: sublocales *}
   161 text {* Interpretation between locales: sublocales *}
   167 
   162 
   168 sublocale lgrp < right: rgrp
   163 sublocale lgrp < right: rgrp
   169 print_facts
   164 print_facts