Mercurial Mercurial > repos > Old_HOL / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -60 +60 +100 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
Mon, 20 Jun 1994 14:52:40 +0200 clasohm added prefix to name of induct axiom changeset | files
Mon, 20 Jun 1994 12:05:03 +0200 nipkow Datatype -> Datatype.ML changeset | files
Fri, 17 Jun 1994 18:34:12 +0200 lcp HOL/Arith/add_left_commute: tidied changeset | files
Fri, 17 Jun 1994 18:32:25 +0200 lcp HOL/HOL.ML/notE: tidied the proof changeset | files
Fri, 17 Jun 1994 18:30:18 +0200 lcp HOL/List/map_append,map_compose: new changeset | files
Fri, 17 Jun 1994 18:28:36 +0200 lcp HOL/ex/NatSum: added another example changeset | files
Fri, 17 Jun 1994 14:16:50 +0200 clasohm adopted to new datatype definition method changeset | files
Fri, 17 Jun 1994 14:15:38 +0200 clasohm datatypes must now be defined using a thy file section changeset | files
Wed, 15 Jun 1994 19:28:35 +0200 nipkow Added set comprehension as a syntactic abbreviation: changeset | files
Wed, 01 Jun 1994 13:24:54 +0200 lcp added test for $ISABELLEBIN=source directory, to changeset | files
Wed, 25 May 1994 13:03:19 +0200 lcp HOL/Arith: definition of diff now uses pred, not nat_rec changeset | files
Wed, 25 May 1994 12:43:50 +0200 lcp HOL/equalities: added some identities from ZF/equalities changeset | files
Wed, 25 May 1994 12:25:40 +0200 lcp HOL/HOL.ML/notE: tidied changeset | files
Thu, 19 May 1994 17:07:19 +0200 wenzelm thy reader now initialised by init_thy_reader(); changeset | files
Fri, 13 May 1994 11:14:20 +0200 lcp HOL/Prod/pair_eq: renamed to Pair_fst_snd_eq changeset | files
Tue, 03 May 1994 15:48:19 +0200 lcp removal of obsolete type-declaration syntax changeset | files
Tue, 03 May 1994 11:30:09 +0200 lcp removal of obsolete type-declaration syntax changeset | files
Sun, 24 Apr 1994 11:27:38 +0200 clasohm renamed theory files isa94 changeset | files
Fri, 22 Apr 1994 21:23:14 +0200 clasohm renamed theory files changeset | files
Thu, 21 Apr 1994 11:28:32 +0200 lcp tidied definitions and proofs changeset | files
Thu, 21 Apr 1994 11:13:22 +0200 lcp HOL/arith.ML/plus_leD1: tidied changeset | files
Tue, 19 Apr 1994 10:50:00 +0200 nipkow changed defns in hol.thy from = to == changeset | files
Wed, 06 Apr 1994 16:31:06 +0200 lcp Now simplifies before the induction changeset | files
Wed, 30 Mar 1994 10:00:23 +0200 nipkow @ now associates to the right, just like #, in order to avoid loss of changeset | files
Sun, 27 Mar 1994 16:43:06 +0200 nipkow Added some sums. changeset | files
Sun, 27 Mar 1994 12:36:39 +0200 nipkow integrated permutative rewriting changeset | files
Tue, 22 Mar 1994 19:55:29 +0100 nipkow used new field "simps" of Datatype changeset | files
Tue, 22 Mar 1994 19:54:55 +0100 nipkow new field "simps" added changeset | files
Tue, 22 Mar 1994 18:07:45 +0100 nipkow added dependency on datatype.ML changeset | files
Tue, 22 Mar 1994 08:32:22 +0100 nipkow Updated simpsets and a few proofs. changeset | files
Tue, 22 Mar 1994 08:31:58 +0100 nipkow Updated simpsets and a few proofs. changeset | files
Tue, 22 Mar 1994 08:28:31 +0100 nipkow Used Datatype functor to define propositional logic terms. changeset | files
Tue, 22 Mar 1994 08:26:25 +0100 nipkow simplified some proofs using ordered rewriting. changeset | files
Tue, 22 Mar 1994 08:25:30 +0100 nipkow used ordered rewriting to simplify some proofs changeset | files
Fri, 18 Mar 1994 20:33:32 +0100 nipkow ML-like datatype decalaration facility. Axiomatic. changeset | files
Fri, 18 Mar 1994 20:32:18 +0100 nipkow added use_thy"Datatype" changeset | files
Thu, 17 Mar 1994 17:02:49 +0100 lcp new type declaration syntax instead of numbers changeset | files
Thu, 17 Mar 1994 14:08:08 +0100 lcp HOL/equalities/Int_Union_image, Un_Inter_image: renamed Int_Union, Un_Inter changeset | files
Thu, 17 Mar 1994 11:27:29 +0100 clasohm adapted type definition to new syntax changeset | files
Wed, 02 Mar 1994 12:26:55 +0100 clasohm changed "." to "$" and Cons to infix "#" to eliminate ambiguity changeset | files
Thu, 24 Feb 1994 14:45:57 +0100 nipkow typo in comment changeset | files
Wed, 23 Feb 1994 10:05:35 +0100 nipkow some more sorting algorithms changeset | files
Wed, 16 Feb 1994 15:13:53 +0100 nipkow added more lemmas (also to nat_ss) changeset | files
Tue, 15 Feb 1994 10:05:17 +0100 nipkow deleted duplicate rewrite rules changeset | files
Tue, 15 Feb 1994 07:55:22 +0100 nipkow added etac FalseE to the simplifier's solver. changeset | files
Sat, 12 Feb 1994 14:46:21 +0100 nipkow added translations for "case xs of" changeset | files
Fri, 11 Feb 1994 11:09:50 +0100 nipkow added ::bool in the defn of True. changeset | files
Thu, 03 Feb 1994 09:55:47 +0100 nipkow Introduction of various new lemmas and of case_tac. changeset | files
Thu, 27 Jan 1994 17:01:10 +0100 nipkow id -> idt in type of @filter and @Alls changeset | files
Wed, 26 Jan 1994 17:53:27 +0100 nipkow sum: renamed case to sum_case changeset | files
Mon, 24 Jan 1994 16:03:03 +0100 nipkow changed header changeset | files
Mon, 24 Jan 1994 16:00:37 +0100 nipkow Verification of quicksort changeset | files
Mon, 24 Jan 1994 15:59:44 +0100 nipkow added qsort changeset | files
Mon, 24 Jan 1994 15:59:02 +0100 nipkow added conj_assoc to HOL_ss changeset | files
Fri, 14 Jan 1994 12:35:27 +0100 lcp commented imageE changeset | files
Fri, 07 Jan 1994 14:23:13 +0100 nipkow added let_weak_cong changeset | files
Fri, 07 Jan 1994 14:22:37 +0100 nipkow added pair_eq changeset | files
Wed, 05 Jan 1994 19:39:05 +0100 nipkow modified solver of HOL_ss to take the new simplifier into account: the thm to changeset | files
Wed, 05 Jan 1994 19:37:07 +0100 nipkow added new rewrite rules to arith_ss changeset | files
Tue, 04 Jan 1994 18:33:20 +0100 nipkow shortened use_thy section taking advantage of dependencies changeset | files
(0) -60 +60 +100 tip
Old_HOL