Fri, 24 Jun 1994 10:45:02 +0200 lcp Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
Thu, 23 Jun 1994 17:52:58 +0200 lcp minor tidying up (ordered rewriting in Integ.ML)
Thu, 23 Jun 1994 17:38:12 +0200 lcp modifications for cardinal arithmetic
Thu, 23 Jun 1994 16:44:57 +0200 lcp Sara\'s perl script for renaming theory files
Tue, 21 Jun 1994 17:20:34 +0200 lcp Addition of cardinals and order types, various tidying
Tue, 21 Jun 1994 16:26:34 +0200 lcp Various updates and tidying
Tue, 21 Jun 1994 11:55:36 +0200 nipkow improved error msg
Mon, 20 Jun 1994 12:25:28 +0200 nipkow Improved error msg "Proved wrong thm"
Mon, 20 Jun 1994 12:13:08 +0200 clasohm parse.ML and scan.ML are now replaced by thy_parse.ML and thy_scan.ML
Mon, 20 Jun 1994 12:03:16 +0200 nipkow Franz Regensburger's changes.
Fri, 17 Jun 1994 17:49:03 +0200 lcp atomize: borrowed HOL version, which checks for both Trueprop
Fri, 17 Jun 1994 17:47:42 +0200 lcp problem 38 is provable
Fri, 17 Jun 1994 16:51:37 +0200 nipkow ordered rewriting applies to conditional rules as well now
Fri, 17 Jun 1994 12:43:24 +0200 clasohm replaced "foldl merge_theories" by "merge_thy_list" in base_on
Thu, 16 Jun 1994 12:07:40 +0200 wenzelm added 'subclass' section;
Thu, 16 Jun 1994 12:06:56 +0200 wenzelm base_on: added 'mk_draft' arg;
Thu, 16 Jun 1994 12:05:53 +0200 wenzelm (beta release)
Thu, 16 Jun 1994 12:04:33 +0200 wenzelm added ext_tsig_subclass, ext_tsig_defsort;
Thu, 16 Jun 1994 12:04:00 +0200 wenzelm added add_classrel;
Thu, 09 Jun 1994 11:11:03 +0200 wenzelm replaced extend_theory;
Thu, 09 Jun 1994 11:09:45 +0200 wenzelm added OldMixfix;
Thu, 09 Jun 1994 11:02:14 +0200 wenzelm workaround bug in Type.expand_typ;
Thu, 09 Jun 1994 11:00:37 +0200 wenzelm new datatype 'mixfix' now pervasive (old one still accesible via OldMixfix);
Thu, 09 Jun 1994 11:00:01 +0200 wenzelm restored functor sig;
Thu, 09 Jun 1994 10:59:20 +0200 wenzelm added axclass.ML, Syntax/mixfix.ML, Thy/thy_syn.ML;
Wed, 01 Jun 1994 15:49:46 +0200 wenzelm added signature constraint;
Wed, 01 Jun 1994 15:47:27 +0200 wenzelm removed garbage;
Wed, 01 Jun 1994 15:46:11 +0200 wenzelm restored old functor name;
Wed, 01 Jun 1994 15:44:56 +0200 wenzelm interface for 'user sections';
Wed, 01 Jun 1994 15:42:25 +0200 wenzelm replaced infix also by |>
Wed, 01 Jun 1994 13:18:35 +0200 lcp added test for $ISABELLEBIN=source directory, to
Wed, 01 Jun 1994 13:11:40 +0200 lcp Improved error messages
Wed, 01 Jun 1994 08:28:12 +0200 nipkow reflected changes in the structure of Thy
Tue, 31 May 1994 13:17:41 +0200 nipkow simpset is hidden in a functor now.
Sun, 29 May 1994 15:14:28 +0200 nipkow Internale optimization of the simplifier: in case a subterm stays unchanged,
Thu, 26 May 1994 16:53:58 +0200 wenzelm axiomatic type class 'package' for Pure (alpha version);
Thu, 26 May 1994 16:51:46 +0200 wenzelm added "axclass.ML", structure AxClass;
Thu, 26 May 1994 16:45:56 +0200 wenzelm added subsort, norm_sort, classes;
Thu, 26 May 1994 16:45:08 +0200 wenzelm replaced "logic" by logicC;
Thu, 26 May 1994 16:43:48 +0200 wenzelm replaced ext_axtab by new_axioms;
Thu, 26 May 1994 16:43:24 +0200 wenzelm added class_triv: theory -> class -> thm (for axclasses);
Thu, 26 May 1994 16:40:45 +0200 wenzelm added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
Thu, 26 May 1994 13:45:43 +0200 clasohm changed syntax of use_string
Thu, 26 May 1994 13:37:51 +0200 clasohm changed use_string's type to string list -> unit because POLY can only
Thu, 26 May 1994 12:55:52 +0200 clasohm "Building new grammar" message is no longer displayed by empty_gram
Tue, 24 May 1994 09:04:03 +0200 nipkow Modified mk_meta_eq to leave meta-equlities on unchanged.
Thu, 19 May 1994 17:06:24 +0200 wenzelm thy reader now initialised by init_thy_reader();
Thu, 19 May 1994 16:42:04 +0200 wenzelm *** empty log message ***
Thu, 19 May 1994 16:30:56 +0200 wenzelm (was Thy/read.ML)
Thu, 19 May 1994 16:27:16 +0200 wenzelm *** empty log message ***
Thu, 19 May 1994 16:26:19 +0200 wenzelm (replaces Thy/parse.ML and Thy/syntax.ML)
Thu, 19 May 1994 16:25:03 +0200 wenzelm (replaces Thy/scan.ML)
Thu, 19 May 1994 16:22:48 +0200 wenzelm new datatype theory, supports 'draft theories' and incremental extension:
Thu, 19 May 1994 16:20:52 +0200 wenzelm added const_type: sg -> typ option;
Thu, 19 May 1994 16:17:46 +0200 wenzelm added print_sign, print_axioms: theory -> unit;
Thu, 19 May 1994 16:16:36 +0200 wenzelm support for new style mixfix annotations;
Thu, 19 May 1994 16:15:38 +0200 wenzelm added incremental extension functions: extend_log_types, extend_type_gram,
Thu, 19 May 1994 16:14:56 +0200 wenzelm added insort_tr, prop_tr' (for axclasses);
Thu, 19 May 1994 16:13:51 +0200 wenzelm replaced fix_aprop by prop_tr';
Thu, 19 May 1994 16:12:37 +0200 wenzelm added infix op also: 'a * ('a -> 'b) -> 'b;
(0) -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip