NEWS
changeset 22376 b711c2ad7507
parent 22316 f662831459de
child 22384 33a46e6c7f04
equal deleted inserted replaced
22375:823f7bee42df 22376:b711c2ad7507
   767 ML {* @{ctyp "'a => 'b"} *}
   767 ML {* @{ctyp "'a => 'b"} *}
   768 ML {* @{cterm "%x. x"} *}
   768 ML {* @{cterm "%x. x"} *}
   769 ML {* @{cprop "x == y"} *}
   769 ML {* @{cprop "x == y"} *}
   770 ML {* @{thm asm_rl} *}
   770 ML {* @{thm asm_rl} *}
   771 ML {* @{thms asm_rl} *}
   771 ML {* @{thms asm_rl} *}
       
   772 ML {* @{const_name c} *}
       
   773 ML {* @{const_syntax c} *}
   772 ML {* @{context} *}
   774 ML {* @{context} *}
   773 ML {* @{theory} *}
   775 ML {* @{theory} *}
   774 ML {* @{theory Pure} *}
   776 ML {* @{theory Pure} *}
   775 ML {* @{simpset} *}
   777 ML {* @{simpset} *}
   776 ML {* @{claset} *}
   778 ML {* @{claset} *}