Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/thy_syntax.ML
Tue, 05 Sep 2000 18:48:41 +0200 wenzelm RecdefPackage.add_recdef_old; file | diff | annotate
Fri, 05 May 2000 22:29:02 +0200 wenzelm added scan_to_id (used to be in Pure/section_utils.ML); file | diff | annotate
Sat, 01 Apr 2000 20:21:39 +0200 wenzelm recdef: admit names/atts; file | diff | annotate
Thu, 30 Mar 2000 19:45:18 +0200 nipkow mod in recdef allows to access the correct simpset via simpset(). file | diff | annotate
Wed, 12 May 1999 17:26:56 +0200 wenzelm strip_quotes replaced by unenclose; file | diff | annotate
Tue, 04 May 1999 16:18:16 +0200 wenzelm add_recdef: removed names / attributes; file | diff | annotate
Fri, 30 Apr 1999 18:09:33 +0200 wenzelm separated recdef / defer_recdef; file | diff | annotate
Tue, 27 Apr 1999 10:51:16 +0200 wenzelm adapted add_inductive, add_record; file | diff | annotate
Fri, 23 Apr 1999 12:22:30 +0200 paulson Now for recdefs that omit the WF relation file | diff | annotate
Thu, 22 Apr 1999 12:49:34 +0200 wenzelm recdef adapted to RecdefPackage.add_recdef; file | diff | annotate
Wed, 14 Apr 1999 14:44:04 +0200 wenzelm intrs: names and atts; file | diff | annotate
Wed, 17 Mar 1999 13:47:04 +0100 wenzelm adapted rep_datatype; file | diff | annotate
Thu, 11 Mar 1999 21:56:22 +0100 wenzelm primrec: empty attributes; file | diff | annotate
Tue, 12 Jan 1999 16:42:21 +0100 wenzelm get_tthms witness theorems; file | diff | annotate
Mon, 28 Dec 1998 16:46:15 +0100 paulson replaced obsolete "trim" by "strip_quotes" file | diff | annotate
Wed, 21 Oct 1998 17:46:00 +0200 berghofe Changed syntax of rep_datatype and inductive: Theorems file | diff | annotate
Fri, 16 Oct 1998 18:50:20 +0200 berghofe Changed structure of name spaces for datatypes. file | diff | annotate
Thu, 30 Jul 1998 23:14:41 +0200 berghofe Fixed primrec. file | diff | annotate
Thu, 30 Jul 1998 22:58:05 +0200 berghofe Fixed primrec. file | diff | annotate
Thu, 30 Jul 1998 17:59:57 +0200 wenzelm fixed primrec; file | diff | annotate
Fri, 24 Jul 1998 13:03:20 +0200 berghofe Adapted to new datatype package. file | diff | annotate
Tue, 30 Jun 1998 20:42:47 +0200 berghofe Adapted to new inductive definition package. file | diff | annotate
Wed, 29 Apr 1998 11:44:30 +0200 wenzelm TypedefPackage.add_typedef; file | diff | annotate
Thu, 08 Jan 1998 18:09:47 +0100 oheimb added split_paired_Ex to the implicit simpset file | diff | annotate
Thu, 13 Nov 1997 15:14:14 +0100 wenzelm fixed record parser; file | diff | annotate
Thu, 13 Nov 1997 12:43:17 +0100 wenzelm improved record syntax; file | diff | annotate
Wed, 12 Nov 1997 12:24:55 +0100 oheimb renamed split_T_case_prem to split_T_case_asm file | diff | annotate
Fri, 07 Nov 1997 08:25:02 +0100 nipkow Each datatype t now proves a theorem split_t_case_prem file | diff | annotate
Mon, 03 Nov 1997 21:13:24 +0100 wenzelm tuned; file | diff | annotate
Mon, 03 Nov 1997 12:24:13 +0100 wenzelm isatool fixclasimp; file | diff | annotate
Thu, 30 Oct 1997 09:45:03 +0100 nipkow For each datatype `t' there is now a theorem `split_t_case' of the form file | diff | annotate
Fri, 24 Oct 1997 17:28:20 +0200 wenzelm record: tuned output; file | diff | annotate
Thu, 23 Oct 1997 12:49:16 +0200 wenzelm added record section; file | diff | annotate
Mon, 20 Oct 1997 11:14:55 +0200 wenzelm adapted to qualified names; file | diff | annotate
Wed, 10 Sep 1997 14:18:12 +0200 nipkow Added Larry's test for preventing a datatype shadowing a theory. file | diff | annotate
Wed, 06 Aug 1997 11:57:52 +0200 wenzelm use ThySyn.add_syntax; file | diff | annotate
Wed, 06 Aug 1997 01:18:31 +0200 berghofe Replaced "init_thy_reader" by "set_parser". file | diff | annotate
Mon, 23 Jun 1997 10:35:49 +0200 paulson New "congs" keyword for recdef theory section file | diff | annotate
Thu, 05 Jun 1997 13:22:25 +0200 paulson A slight simplification of optstring file | diff | annotate
Mon, 26 May 1997 12:42:38 +0200 paulson Now recdef checks the name of the function being defined. file | diff | annotate
Fri, 23 May 1997 09:17:26 +0200 nipkow Added overloaded function `size' for all datatypes. file | diff | annotate
Thu, 15 May 1997 12:53:12 +0200 paulson TFL theory section file | diff | annotate
Thu, 10 Apr 1997 12:20:55 +0200 nipkow Turned Addsimps into AddIffs for datatype laws. file | diff | annotate
Wed, 09 Apr 1997 12:32:04 +0200 paulson Using Blast_tac file | diff | annotate
Fri, 05 Jul 1996 14:22:59 +0200 berghofe Simplified syntax of primrec definitions. file | diff | annotate
Thu, 06 Jun 1996 13:13:18 +0200 paulson Quotes now optional around inductive set file | diff | annotate
Fri, 19 Apr 1996 11:33:24 +0200 clasohm added Konrad's code for the datatype package file | diff | annotate
Wed, 13 Mar 1996 11:55:25 +0100 clasohm modified primrec so it can be used in MiniML/Type.thy file | diff | annotate
Mon, 05 Feb 1996 21:27:16 +0100 clasohm expanded tabs; renamed subtype to typedef; file | diff | annotate
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs file | diff | annotate
Tue, 02 Jan 1996 10:46:50 +0100 paulson Improving space efficiency of inductive/datatype definitions. file | diff | annotate
Thu, 02 Nov 1995 12:45:58 +0100 clasohm extended complex_typ file | diff | annotate
Wed, 04 Oct 1995 13:10:03 +0100 clasohm added local simpsets; removed IOA from 'make test' file | diff | annotate
Fri, 08 Sep 1995 13:23:04 +0200 clasohm added nested types on right hand side of datatype definitions file | diff | annotate
Tue, 28 Mar 1995 12:25:20 +0200 clasohm changed syntax of datatype declarations (curried types for constructor file | diff | annotate
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application file | diff | annotate
less more (0) tip
isabelle