1994-07-15 clasohm added thy_name to Datatype_Fun's parameter
1994-07-15 clasohm added check for concistency of filename and theory name;
1994-07-15 clasohm added function mapst
1994-07-14 wenzelm added functor signature constraint;
1994-07-14 wenzelm minor internal renamings;
1994-07-14 wenzelm changed syntax "(| _ : _ |)" to "OFCLASS(_, _)";
1994-07-13 lcp indentation and renaming of rules
1994-07-12 lcp minor updates
1994-07-12 lcp chain_tac: deleted; just use etac mp
1994-07-12 lcp Improved error checking
1994-07-12 lcp new cardinal arithmetic developments
1994-07-12 clasohm removed flatten_typ and replaced add_consts by add_consts_i
1994-07-12 nipkow Corrected HOL.tex
1994-07-12 nipkow added datatype section
1994-07-12 nipkow included rail.sty
1994-07-11 nipkow Initial revision
1994-07-11 lcp minor edits
1994-07-11 lcp restoring after deletion
1994-07-11 lcp minor edits
1994-07-11 nipkow type constraints
1994-07-11 lcp documented subgoals_tac
1994-07-11 lcp New errata list for the documentation
1994-07-11 lcp misc updates
1994-07-11 clasohm removed flatten_term and replaced add_axioms by add_axioms_i
1994-07-07 nipkow added () around some of the ::
1994-07-07 nipkow changed priority of ::
1994-07-06 wenzelm exported opt_infix, opt_mixfix parsers;
1994-07-06 wenzelm added raw_unify;
1994-07-06 wenzelm various minor changes (names and comments);
1994-07-06 clasohm changed comment for const_name
1994-07-06 wenzelm changed comment only;
1994-07-01 clasohm rewritec now uses trace_thm for it's "rewrite rule from different theory"
1994-07-01 clasohm changed syntax of datatype declaration
1994-07-01 clasohm replaced extend_theory by new add_* functions;
1994-06-29 clasohm added parentheses made necessary by new constrain precedence
1994-06-29 clasohm added parentheses made necessary by change of constrain's precedence
1994-06-29 clasohm changed precedence of constrain to [4, 0], 3
1994-06-24 lcp FOL/FOL.ML/excluded_middle_tac: new
1994-06-24 lcp Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
1994-06-23 lcp minor tidying up (ordered rewriting in Integ.ML)
1994-06-23 lcp modifications for cardinal arithmetic
1994-06-23 lcp Sara\'s perl script for renaming theory files
1994-06-21 lcp Addition of cardinals and order types, various tidying
1994-06-21 lcp Various updates and tidying
1994-06-21 nipkow improved error msg
1994-06-20 nipkow Improved error msg "Proved wrong thm"
1994-06-20 clasohm parse.ML and scan.ML are now replaced by thy_parse.ML and thy_scan.ML
1994-06-20 nipkow Franz Regensburger's changes.
1994-06-17 lcp atomize: borrowed HOL version, which checks for both Trueprop
1994-06-17 lcp problem 38 is provable
1994-06-17 nipkow ordered rewriting applies to conditional rules as well now
1994-06-17 clasohm replaced "foldl merge_theories" by "merge_thy_list" in base_on
1994-06-16 wenzelm added 'subclass' section;
1994-06-16 wenzelm base_on: added 'mk_draft' arg;
1994-06-16 wenzelm (beta release)
1994-06-16 wenzelm added ext_tsig_subclass, ext_tsig_defsort;
1994-06-16 wenzelm added add_classrel;
1994-06-09 wenzelm replaced extend_theory;
1994-06-09 wenzelm added OldMixfix;
1994-06-09 wenzelm workaround bug in Type.expand_typ;
(0) -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip