| Fri, 25 Nov 1994 11:02:39 +0100 |
lcp |
moved Cantors theorem here from ZF/ex/misc
|
changeset |
files
|
| Fri, 25 Nov 1994 10:43:50 +0100 |
lcp |
deepen_tac: modified due to outcome of experiments. Its
|
changeset |
files
|
| Fri, 25 Nov 1994 09:13:49 +0100 |
clasohm |
added qed_goal[w]
|
changeset |
files
|
| Fri, 25 Nov 1994 00:02:37 +0100 |
lcp |
added blank line
|
changeset |
files
|
| Fri, 25 Nov 1994 00:01:04 +0100 |
lcp |
tidied proofs, using fast_tac etc. as much as possible
|
changeset |
files
|
| Fri, 25 Nov 1994 00:00:35 +0100 |
lcp |
prove_fun: new; no longer depends upon the version in simpdata.ML
|
changeset |
files
|
| Thu, 24 Nov 1994 10:57:24 +0100 |
lcp |
data_domain,Codata_domain: removed replicate; now return one
|
changeset |
files
|
| Thu, 24 Nov 1994 10:53:46 +0100 |
lcp |
tidied proofs, using fast_tac etc. as much as possible
|
changeset |
files
|
| Thu, 24 Nov 1994 10:47:45 +0100 |
lcp |
added comments on alternative uses of type_intrs/elims
|
changeset |
files
|
| Thu, 24 Nov 1994 10:38:08 +0100 |
lcp |
modified for new treatment of mutual recursion
|
changeset |
files
|
| Thu, 24 Nov 1994 10:31:47 +0100 |
lcp |
the_equality: more careful use of addSIs and addIs
|
changeset |
files
|
| Thu, 24 Nov 1994 10:23:41 +0100 |
lcp |
cons_fun_eq: modified strange uses of classical reasoner
|
changeset |
files
|
| Thu, 24 Nov 1994 00:33:13 +0100 |
lcp |
moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML
|
changeset |
files
|
| Thu, 24 Nov 1994 00:32:43 +0100 |
lcp |
moved version of Cantors theorem to ZF/Perm.ML
|
changeset |
files
|
| Thu, 24 Nov 1994 00:32:12 +0100 |
lcp |
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
|
changeset |
files
|
| Thu, 24 Nov 1994 00:31:41 +0100 |
lcp |
ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
|
changeset |
files
|
| Thu, 24 Nov 1994 00:31:08 +0100 |
lcp |
updated for new deepen_tac
|
changeset |
files
|
| Thu, 24 Nov 1994 00:30:35 +0100 |
lcp |
trivial changes
|
changeset |
files
|
| Wed, 23 Nov 1994 11:45:56 +0100 |
lcp |
new reference to HO patterns
|
changeset |
files
|
| Tue, 22 Nov 1994 23:32:16 +0100 |
lcp |
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
|
changeset |
files
|
| Tue, 22 Nov 1994 23:30:49 +0100 |
lcp |
Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars
|
changeset |
files
|
| Mon, 21 Nov 1994 18:48:03 +0100 |
lcp |
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
|
changeset |
files
|
| Mon, 21 Nov 1994 15:53:02 +0100 |
lcp |
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
|
changeset |
files
|
| Mon, 21 Nov 1994 14:11:21 +0100 |
clasohm |
replaced 'val ... = result();' by 'qed "...";'
|
changeset |
files
|
| Mon, 21 Nov 1994 14:06:59 +0100 |
lcp |
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
|
changeset |
files
|
| Mon, 21 Nov 1994 13:47:00 +0100 |
lcp |
ZF/EquivClass/congruent_commuteI: uncommented and simplified proof
|
changeset |
files
|
| Mon, 21 Nov 1994 13:09:41 +0100 |
lcp |
ZF/ZF.ML/UN_iff, INT_iff: added to the signature
|
changeset |
files
|
| Mon, 21 Nov 1994 11:49:36 +0100 |
lcp |
Pure/thm/norm_term_skip: new, for skipping normalization of the context
|
changeset |
files
|
| Mon, 21 Nov 1994 11:33:23 +0100 |
lcp |
Pure/sequence: added comment explaining that memoing sequences were found
|
changeset |
files
|
| Mon, 21 Nov 1994 11:27:10 +0100 |
lcp |
Pure/envir/norm_term: replaced equality test for [] by null
|
changeset |
files
|