Fri, 24 Feb 1995 11:52:19 +0100 clasohm added ExcludeThm; cleaned up Makefile; fixed isalpha bug (replaced by isalnum)
Fri, 17 Feb 1995 13:25:11 +0100 clasohm added check "length ts > 1" before printing ambiguity warning in infer_types
Thu, 16 Feb 1995 08:55:15 +0100 nipkow Improved test for looping rewrite rules.
Wed, 15 Feb 1995 20:02:47 +0100 regensbu replaced pair_ss by prod_ss
Wed, 08 Feb 1995 11:30:00 +0100 nipkow Improved check for looping conditional rewrite rules.
Tue, 07 Feb 1995 17:36:48 +0100 regensbu ID for the file
Tue, 07 Feb 1995 17:35:49 +0100 regensbu ID for the file
Tue, 07 Feb 1995 17:30:34 +0100 regensbu 'get ID update working'
Tue, 07 Feb 1995 17:26:32 +0100 regensbu CVS:
Tue, 07 Feb 1995 17:25:31 +0100 regensbu CVS:
Tue, 07 Feb 1995 11:59:32 +0100 clasohm added qed, qed_goal[w]
Fri, 03 Feb 1995 12:32:14 +0100 clasohm added specification of csh as script interpreter
Thu, 02 Feb 1995 13:11:51 +0100 clasohm simplified elimination of chain productions
Fri, 27 Jan 1995 13:40:07 +0100 wenzelm binder: optional body pri now [bracketted];
Fri, 27 Jan 1995 13:35:29 +0100 wenzelm improved read_xrules: patterns no longer read twice;
Fri, 27 Jan 1995 13:33:52 +0100 wenzelm *** empty log message ***
Fri, 27 Jan 1995 13:31:26 +0100 wenzelm instance: now automatically includes defs of current thy node as witnesses;
Fri, 27 Jan 1995 13:29:44 +0100 wenzelm binder: optional body pri now [bracketted];
Fri, 27 Jan 1995 12:42:03 +0100 clasohm added documentation of pwd
Fri, 27 Jan 1995 12:31:18 +0100 clasohm renamed Sign.ambiguity_level to Syntax.ambiguity_level
Fri, 27 Jan 1995 12:30:36 +0100 clasohm moved ambiguity_level from sign.ML to Syntax/syntax.ML
Fri, 27 Jan 1995 12:28:05 +0100 clasohm moved ambiguity_level to Syntax/syntax.ML
Thu, 26 Jan 1995 13:31:36 +0100 clasohm added documentation of Sign.ambiguity_level
Thu, 26 Jan 1995 12:44:50 +0100 clasohm added reference variable ambiguity_level to control ambiguity warnings
Wed, 25 Jan 1995 04:00:27 +0100 lcp changed due to new .bib files
Tue, 24 Jan 1995 12:17:49 +0100 clasohm added optional body priority to binder declaration
Tue, 24 Jan 1995 03:04:20 +0100 lcp Under RS added cross reference to bind_thm
Tue, 24 Jan 1995 03:03:19 +0100 lcp documented slow_tac, slow_best_tac, depth_tac, deepen_tac
Tue, 24 Jan 1995 03:02:01 +0100 lcp removed mention of FOL_dup_cs
Tue, 24 Jan 1995 03:01:14 +0100 lcp \bibliography now includes crossref.bib
Tue, 24 Jan 1995 03:00:32 +0100 lcp updates for Isabelle94-2
Mon, 23 Jan 1995 12:20:10 +0100 clasohm simplified get_thm a bit
Fri, 20 Jan 1995 10:41:01 +0100 lcp Replaced ordermap_z_lepoll by ordermap_z_lt, which is
Fri, 20 Jan 1995 02:00:57 +0100 lcp README: Now documents to Tools directory
Fri, 20 Jan 1995 02:00:23 +0100 lcp Deleted semicolon at the end of the qed_goal line, which was preventing
Thu, 19 Jan 1995 19:46:49 +0100 nipkow some cosmetic changes
Thu, 19 Jan 1995 16:05:21 +0100 clasohm added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
Wed, 18 Jan 1995 11:36:04 +0100 clasohm added optional precedence for body of binder;
Wed, 18 Jan 1995 10:17:55 +0100 wenzelm quite a lot of minor and major revisions (inspecting theories, read_axm,
Fri, 13 Jan 1995 02:02:00 +0100 lcp empty_def typo Isabelle94-2
Fri, 13 Jan 1995 02:01:26 +0100 lcp Proved comp_lam.
Fri, 13 Jan 1995 02:00:43 +0100 lcp Corrected indexing of *datatype
Thu, 12 Jan 1995 10:53:42 +0100 lcp prove_fun now includes equalityI. Added the rewrite rules
Thu, 12 Jan 1995 10:39:47 +0100 lcp Proved sum_bij, sum_ord_iso_cong, prod_bij,
Thu, 12 Jan 1995 03:04:10 +0100 lcp Proved case_cong and case_case.
Thu, 12 Jan 1995 03:03:45 +0100 lcp Renamed single_fun to singleton_fun.
Thu, 12 Jan 1995 03:03:25 +0100 lcp Now also depends upon equalities.thy, allowing use of the
Thu, 12 Jan 1995 03:03:07 +0100 lcp Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
Thu, 12 Jan 1995 03:02:34 +0100 lcp Removed spurious comment about eq_cs
Thu, 12 Jan 1995 03:02:05 +0100 lcp Moved theorems Ord_cases_lemma and Ord_cases to Ordinal.ML
Thu, 12 Jan 1995 03:01:40 +0100 lcp Now depends upon Bool, so that 1 and 2 are defined
Thu, 12 Jan 1995 03:01:20 +0100 lcp Moved theorems Ord_cases_lemma and Ord_cases here from Univ,
Thu, 12 Jan 1995 03:00:58 +0100 lcp Added constants Ord_alt, ++, **
Thu, 12 Jan 1995 03:00:38 +0100 lcp Proved equivalence of Ord and Ord_alt. Proved
Wed, 11 Jan 1995 18:47:03 +0100 lcp Proved ord_isoI, ord_iso_refl. Simplified proof of
Wed, 11 Jan 1995 18:42:06 +0100 lcp Proved cadd_cmult_distrib.
Wed, 11 Jan 1995 18:30:37 +0100 lcp Now proof of Ord_jump_cardinal uses
Wed, 11 Jan 1995 18:21:39 +0100 lcp Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
Wed, 11 Jan 1995 13:25:23 +0100 wenzelm pretty_gram: now sorts productions;
Wed, 11 Jan 1995 10:57:39 +0100 wenzelm removed print_sign, print_axioms;
(0) -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip