Thu, 24 Apr 1997 18:06:46 +0200 | nipkow | Introduced a generic "induct_tac" which picks up the right induction scheme | file | diff | annotate |
Wed, 29 Jan 1997 15:32:18 +0100 | paulson | Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work | file | diff | annotate |
Tue, 07 May 1996 09:58:12 +0200 | berghofe | Added function claset_of. | file | diff | annotate |
Fri, 19 Apr 1996 11:33:24 +0200 | clasohm | added Konrad's code for the datatype package | file | diff | annotate |
Fri, 12 Apr 1996 12:41:26 +0200 | clasohm | changed first parameter of add_thydata and get_thydata | file | diff | annotate |
Tue, 30 Jan 1996 15:24:36 +0100 | clasohm | expanded tabs | file | diff | annotate |
Mon, 29 Jan 1996 13:48:37 +0100 | clasohm | changed the way simpsets and information about datatypes are stored | file | diff | annotate |