wenzelm [Sat, 18 Jun 2005 22:41:18 +0200] rev 16465
added Pure/General/ord_list.ML;
wenzelm [Sat, 18 Jun 2005 22:40:51 +0200] rev 16464
Ordered lists without duplicates.
huffman [Sat, 18 Jun 2005 00:38:18 +0200] rev 16463
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman [Sat, 18 Jun 2005 00:33:27 +0200] rev 16462
make match_rews into simp rules by default
huffman [Fri, 17 Jun 2005 21:19:31 +0200] rev 16461
support theorem names and attributes for fixrec equations; also make them into simp rules by default, like primrec does
huffman [Fri, 17 Jun 2005 18:50:40 +0200] rev 16460
added match functions for ONE, TT, and FF; added theorem mplus_fail2
wenzelm [Fri, 17 Jun 2005 18:36:25 +0200] rev 16459
updated;
wenzelm [Fri, 17 Jun 2005 18:35:27 +0200] rev 16458
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
wenzelm [Fri, 17 Jun 2005 18:33:42 +0200] rev 16457
Context.names_of;
wenzelm [Fri, 17 Jun 2005 18:33:41 +0200] rev 16456
* Pure/TheoryDataFun: change of the argument structure;
* Pure/TheoryDataFun: change of the argument structure -- got rid of Sign.sg;