| Wed, 29 Jun 1994 12:01:17 +0200 |
clasohm |
changed precedence of constrain to [4, 0], 3
|
changeset |
files
|
| Fri, 24 Jun 1994 13:01:53 +0200 |
lcp |
FOL/FOL.ML/excluded_middle_tac: new
|
changeset |
files
|
| Fri, 24 Jun 1994 10:45:02 +0200 |
lcp |
Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
|
changeset |
files
|
| Thu, 23 Jun 1994 17:52:58 +0200 |
lcp |
minor tidying up (ordered rewriting in Integ.ML)
|
changeset |
files
|
| Thu, 23 Jun 1994 17:38:12 +0200 |
lcp |
modifications for cardinal arithmetic
|
changeset |
files
|
| Thu, 23 Jun 1994 16:44:57 +0200 |
lcp |
Sara\'s perl script for renaming theory files
|
changeset |
files
|
| Tue, 21 Jun 1994 17:20:34 +0200 |
lcp |
Addition of cardinals and order types, various tidying
|
changeset |
files
|
| Tue, 21 Jun 1994 16:26:34 +0200 |
lcp |
Various updates and tidying
|
changeset |
files
|
| Tue, 21 Jun 1994 11:55:36 +0200 |
nipkow |
improved error msg
|
changeset |
files
|
| Mon, 20 Jun 1994 12:25:28 +0200 |
nipkow |
Improved error msg "Proved wrong thm"
|
changeset |
files
|
| 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
|
changeset |
files
|
| Mon, 20 Jun 1994 12:03:16 +0200 |
nipkow |
Franz Regensburger's changes.
|
changeset |
files
|
| Fri, 17 Jun 1994 17:49:03 +0200 |
lcp |
atomize: borrowed HOL version, which checks for both Trueprop
|
changeset |
files
|
| Fri, 17 Jun 1994 17:47:42 +0200 |
lcp |
problem 38 is provable
|
changeset |
files
|