wenzelm [Wed, 14 Dec 1994 10:32:07 +0100] rev 201
improved primrec: now calls store_thm;
clasohm [Fri, 09 Dec 1994 13:39:05 +0100] rev 200
removed HOL_Lemmas structure and added qed_goal
clasohm [Thu, 08 Dec 1994 12:50:38 +0100] rev 199
replaced store_thm by bind_thm
nipkow [Wed, 07 Dec 1994 14:12:27 +0100] rev 198
Added (? x. x=t & P) = P to the simpset.
nipkow [Wed, 07 Dec 1994 14:11:22 +0100] rev 197
Removed a local lemma which is now part of HOL_ss.
nipkow [Fri, 02 Dec 1994 16:13:34 +0100] rev 196
Moved the old List to ex and replaced it by one defined via
datatype and primrec. List does not depend on Sexp any more.
Had to modify the datatype-grammar to allow "[]" ("[]"). Does not allow
strings but only ids as type constructors. This is consistent with the
documentation and merely undoes an extension of Markus's.
nipkow [Fri, 02 Dec 1994 16:09:49 +0100] rev 195
Moved HOL/List to HOL/ex/SList (strict list).
Modified sons on (S)List accordingly.
nipkow [Fri, 02 Dec 1994 11:43:20 +0100] rev 194
small updates because datatype list is now used. In particular Nil -> []
nipkow [Fri, 02 Dec 1994 10:26:59 +0100] rev 193
list_ind_tac -> list.induct_tac
nipkow [Thu, 01 Dec 1994 17:35:03 +0100] rev 192
Added dependency on thy_syntax.ML