Mon, 11 Jul 1994 13:15:05 +0200 removed flatten_term and replaced add_axioms by add_axioms_i
clasohm [Mon, 11 Jul 1994 13:15:05 +0200] rev 454
removed flatten_term and replaced add_axioms by add_axioms_i
Thu, 07 Jul 1994 19:47:34 +0200 added () around some of the ::
nipkow [Thu, 07 Jul 1994 19:47:34 +0200] rev 453
added () around some of the ::
Thu, 07 Jul 1994 19:22:49 +0200 changed priority of ::
nipkow [Thu, 07 Jul 1994 19:22:49 +0200] rev 452
changed priority of ::
Wed, 06 Jul 1994 14:39:32 +0200 exported opt_infix, opt_mixfix parsers;
wenzelm [Wed, 06 Jul 1994 14:39:32 +0200] rev 451
exported opt_infix, opt_mixfix parsers; removed 'subclass' section (now handled by 'instance'); improved make_syntax: section names now added automatically to keywords;
Wed, 06 Jul 1994 12:51:27 +0200 added raw_unify;
wenzelm [Wed, 06 Jul 1994 12:51:27 +0200] rev 450
added raw_unify;
Wed, 06 Jul 1994 12:49:56 +0200 various minor changes (names and comments);
wenzelm [Wed, 06 Jul 1994 12:49:56 +0200] rev 449
various minor changes (names and comments);
Wed, 06 Jul 1994 11:53:30 +0200 changed comment for const_name
clasohm [Wed, 06 Jul 1994 11:53:30 +0200] rev 448
changed comment for const_name
Wed, 06 Jul 1994 11:36:00 +0200 changed comment only;
wenzelm [Wed, 06 Jul 1994 11:36:00 +0200] rev 447
changed comment only;
Fri, 01 Jul 1994 11:10:31 +0200 rewritec now uses trace_thm for it's "rewrite rule from different theory"
clasohm [Fri, 01 Jul 1994 11:10:31 +0200] rev 446
rewritec now uses trace_thm for it's "rewrite rule from different theory" message
Fri, 01 Jul 1994 11:04:12 +0200 changed syntax of datatype declaration
clasohm [Fri, 01 Jul 1994 11:04:12 +0200] rev 445
changed syntax of datatype declaration
Fri, 01 Jul 1994 11:03:42 +0200 replaced extend_theory by new add_* functions;
clasohm [Fri, 01 Jul 1994 11:03:42 +0200] rev 444
replaced extend_theory by new add_* functions; changed syntax of datatype declaration
Wed, 29 Jun 1994 12:13:03 +0200 added parentheses made necessary by new constrain precedence
clasohm [Wed, 29 Jun 1994 12:13:03 +0200] rev 443
added parentheses made necessary by new constrain precedence
Wed, 29 Jun 1994 12:03:41 +0200 added parentheses made necessary by change of constrain's precedence
clasohm [Wed, 29 Jun 1994 12:03:41 +0200] rev 442
added parentheses made necessary by change of constrain's precedence
Wed, 29 Jun 1994 12:01:17 +0200 changed precedence of constrain to [4, 0], 3
clasohm [Wed, 29 Jun 1994 12:01:17 +0200] rev 441
changed precedence of constrain to [4, 0], 3
Fri, 24 Jun 1994 13:01:53 +0200 FOL/FOL.ML/excluded_middle_tac: new
lcp [Fri, 24 Jun 1994 13:01:53 +0200] rev 440
FOL/FOL.ML/excluded_middle_tac: new
Fri, 24 Jun 1994 10:45:02 +0200 Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
lcp [Fri, 24 Jun 1994 10:45:02 +0200] rev 439
Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
Thu, 23 Jun 1994 17:52:58 +0200 minor tidying up (ordered rewriting in Integ.ML)
lcp [Thu, 23 Jun 1994 17:52:58 +0200] rev 438
minor tidying up (ordered rewriting in Integ.ML)
Thu, 23 Jun 1994 17:38:12 +0200 modifications for cardinal arithmetic
lcp [Thu, 23 Jun 1994 17:38:12 +0200] rev 437
modifications for cardinal arithmetic
Thu, 23 Jun 1994 16:44:57 +0200 Sara\'s perl script for renaming theory files
lcp [Thu, 23 Jun 1994 16:44:57 +0200] rev 436
Sara\'s perl script for renaming theory files
Tue, 21 Jun 1994 17:20:34 +0200 Addition of cardinals and order types, various tidying
lcp [Tue, 21 Jun 1994 17:20:34 +0200] rev 435
Addition of cardinals and order types, various tidying
Tue, 21 Jun 1994 16:26:34 +0200 Various updates and tidying
lcp [Tue, 21 Jun 1994 16:26:34 +0200] rev 434
Various updates and tidying
Tue, 21 Jun 1994 11:55:36 +0200 improved error msg
nipkow [Tue, 21 Jun 1994 11:55:36 +0200] rev 433
improved error msg
Mon, 20 Jun 1994 12:25:28 +0200 Improved error msg "Proved wrong thm"
nipkow [Mon, 20 Jun 1994 12:25:28 +0200] rev 432
Improved error msg "Proved wrong thm"
Mon, 20 Jun 1994 12:13:08 +0200 parse.ML and scan.ML are now replaced by thy_parse.ML and thy_scan.ML
clasohm [Mon, 20 Jun 1994 12:13:08 +0200] rev 431
parse.ML and scan.ML are now replaced by thy_parse.ML and thy_scan.ML
Mon, 20 Jun 1994 12:03:16 +0200 Franz Regensburger's changes.
nipkow [Mon, 20 Jun 1994 12:03:16 +0200] rev 430
Franz Regensburger's changes.
Fri, 17 Jun 1994 17:49:03 +0200 atomize: borrowed HOL version, which checks for both Trueprop
lcp [Fri, 17 Jun 1994 17:49:03 +0200] rev 429
atomize: borrowed HOL version, which checks for both Trueprop and == as main connective (avoids using wildcard)
Fri, 17 Jun 1994 17:47:42 +0200 problem 38 is provable
lcp [Fri, 17 Jun 1994 17:47:42 +0200] rev 428
problem 38 is provable
Fri, 17 Jun 1994 16:51:37 +0200 ordered rewriting applies to conditional rules as well now
nipkow [Fri, 17 Jun 1994 16:51:37 +0200] rev 427
ordered rewriting applies to conditional rules as well now
Fri, 17 Jun 1994 12:43:24 +0200 replaced "foldl merge_theories" by "merge_thy_list" in base_on
clasohm [Fri, 17 Jun 1994 12:43:24 +0200] rev 426
replaced "foldl merge_theories" by "merge_thy_list" in base_on
Thu, 16 Jun 1994 12:07:40 +0200 added 'subclass' section;
wenzelm [Thu, 16 Jun 1994 12:07:40 +0200] rev 425
added 'subclass' section; minor internal cleanups;
(0) -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip