src/HOL/ex/LocaleTest2.thy
changeset 29586 4f9803829625
parent 29233 ce6d35a0bed6
child 30729 461ee3e49ad3
equal deleted inserted replaced
29585:c23295521af5 29586:4f9803829625
   622 lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)"
   622 lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)"
   623   apply (rule nat_dvd.less_def) done
   623   apply (rule nat_dvd.less_def) done
   624 thm nat_dvd.meet_left text {* from dlat *}
   624 thm nat_dvd.meet_left text {* from dlat *}
   625 lemma "gcd x y dvd x"
   625 lemma "gcd x y dvd x"
   626   apply (rule nat_dvd.meet_left) done
   626   apply (rule nat_dvd.meet_left) done
   627 
       
   628 print_interps dpo
       
   629 print_interps dlat
       
   630 
   627 
   631 
   628 
   632 subsection {* Group example with defined operations @{text inv} and @{text unit} *}
   629 subsection {* Group example with defined operations @{text inv} and @{text unit} *}
   633 
   630 
   634 subsubsection {* Locale declarations and lemmas *}
   631 subsubsection {* Locale declarations and lemmas *}