src/HOLCF/Porder0.thy
changeset 2394 91d8abf108be
parent 2291 fbd14a05fb88
child 2640 ee4dfce170a0
equal deleted inserted replaced
2393:651fce76c86c 2394:91d8abf108be
    18 (* default type is still term ! *)
    18 (* default type is still term ! *)
    19 (* void is the prototype in po *)
    19 (* void is the prototype in po *)
    20 
    20 
    21 arities void :: po
    21 arities void :: po
    22 
    22 
    23 consts  "<<"    ::      "['a,'a::po] => bool"   (infixl 55)
    23 consts
       
    24 
       
    25   "<<"		:: "['a,'a::po] => bool"	(infixl 55)
       
    26 
       
    27 syntax (symbols)
       
    28 
       
    29   "op <<"	:: "['a,'a::po] => bool"	(infixl "\\<sqsubseteq>" 55)
    24 
    30 
    25 rules
    31 rules
    26 
    32 
    27 (* class axioms: justification is theory Void *)
    33 (* class axioms: justification is theory Void *)
    28 
    34 
    29 refl_less       "x << x"        
    35 refl_less       "x<<x"        
    30                                 (* witness refl_less_void    *)
    36                                 (* witness refl_less_void    *)
    31 
    37 
    32 antisym_less    "[|x<<y ; y<<x |] ==> x = y"    
    38 antisym_less    "[|x<<y ; y<<x |] ==> x = y"    
    33                                 (* witness antisym_less_void *)
    39                                 (* witness antisym_less_void *)
    34 
    40 
    37 
    43 
    38 (* instance of << for the prototype void *)
    44 (* instance of << for the prototype void *)
    39 
    45 
    40 inst_void_po    "((op <<)::[void,void]=>bool) = less_void"
    46 inst_void_po    "((op <<)::[void,void]=>bool) = less_void"
    41 
    47 
    42 (* start 8bit 1 *)
       
    43 (* end 8bit 1 *)
       
    44 
       
    45 end 
    48 end 
    46 
    49 
    47 
    50 
    48 
    51 
    49 
    52