Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Orderings.thy
changeset 26324 456f726a11e4
parent 26300 03def556e26e
child 26496 49ae9456eba9
equal deleted inserted replaced
26323:73efc70edeef 26324:456f726a11e4 
   923   leave out the "(xtrans)" above.
 
   923   leave out the "(xtrans)" above.
 
   924 *)
 
   924 *)
 
   925 
   925 
   926 subsection {* Order on bool *}
 
   926 subsection {* Order on bool *}
 
   927 
   927 
   928 instantiation bool :: order 
   928 instantiation bool :: order
 
   929 begin
 
   929 begin
 
   930 
   930 
   931 definition
 
   931 definition
 
   932   le_bool_def [code func del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
 
   932   le_bool_def [code func del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
 
   933 
   933
isabelle