| Thu, 08 Dec 1994 14:18:31 +0100 |
lcp |
UN_upper_cardinal: updated to refer to Card_le_imp_lepoll
|
changeset |
files
|
| Thu, 08 Dec 1994 14:06:16 +0100 |
lcp |
sum_lepoll_self, cadd_le_self, prod_lepoll_self,
|
changeset |
files
|
| Thu, 08 Dec 1994 13:53:28 +0100 |
lcp |
le_imp_lepoll: renamed to Card_le_imp_lepoll
|
changeset |
files
|
| Thu, 08 Dec 1994 13:38:13 +0100 |
lcp |
Card_cardinal_le: new
|
changeset |
files
|
| Thu, 08 Dec 1994 12:46:25 +0100 |
clasohm |
changed Pure's grammar and the way types are converted to nonterminals
|
changeset |
files
|
| Thu, 08 Dec 1994 12:45:28 +0100 |
clasohm |
replaced type_syn by pure_syn in Pure signature
|
changeset |
files
|
| Thu, 08 Dec 1994 11:28:34 +0100 |
lcp |
test_assume_tac: now tries eq_assume_tac on exceptional cases
|
changeset |
files
|
| Thu, 08 Dec 1994 11:26:25 +0100 |
lcp |
res_inst_tac: added comments
|
changeset |
files
|
| Wed, 07 Dec 1994 13:12:04 +0100 |
clasohm |
added qed and qed_goal[w]
|
changeset |
files
|
| Wed, 07 Dec 1994 12:34:47 +0100 |
clasohm |
moved first call of store_theory from thy_read.ML to created .thy.ML file
|
changeset |
files
|
| Tue, 06 Dec 1994 12:50:13 +0100 |
clasohm |
added bind_thm
|
changeset |
files
|
| Wed, 30 Nov 1994 13:53:46 +0100 |
clasohm |
added qed and qed_goal[w]
|
changeset |
files
|
| Wed, 30 Nov 1994 13:18:42 +0100 |
clasohm |
added qed_goal for meta_iffD
|
changeset |
files
|
| Wed, 30 Nov 1994 13:13:52 +0100 |
clasohm |
replaced "val ... = result()" by "qed ..."
|
changeset |
files
|
| Tue, 29 Nov 1994 11:51:07 +0100 |
lcp |
le_UN_Ord_lt_csucc: added comment
|
changeset |
files
|
| Tue, 29 Nov 1994 00:31:31 +0100 |
lcp |
replaced "rules" by "defs"
|
changeset |
files
|
| Mon, 28 Nov 1994 19:48:30 +0100 |
regensbu |
----------------------------------------------------------------------
|
changeset |
files
|
| Fri, 25 Nov 1994 11:13:55 +0100 |
lcp |
ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any
|
changeset |
files
|
| Fri, 25 Nov 1994 11:08:12 +0100 |
lcp |
checks that the recursive sets are Consts before taking
|
changeset |
files
|
| Fri, 25 Nov 1994 11:04:44 +0100 |
lcp |
equiv_comp_eq: simplified proof
|
changeset |
files
|
| 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
|
| Mon, 21 Nov 1994 10:51:40 +0100 |
lcp |
page 157 erratum
|
changeset |
files
|
| Mon, 21 Nov 1994 10:39:32 +0100 |
lcp |
now searches all subdirectories of object-logics
|
changeset |
files
|
| Fri, 18 Nov 1994 13:14:23 +0100 |
nipkow |
Chnaged simplifier description (lhss)
|
changeset |
files
|
| Fri, 18 Nov 1994 13:08:10 +0100 |
clasohm |
added call of store_theory after thy file has been read
|
changeset |
files
|
| Fri, 18 Nov 1994 13:04:51 +0100 |
nipkow |
Updated description of valid lhss.
|
changeset |
files
|
| Thu, 17 Nov 1994 22:01:08 +0100 |
lcp |
In ZF, type i has class term, not (just) logic
|
changeset |
files
|
| Mon, 14 Nov 1994 14:47:20 +0100 |
clasohm |
added check for newlines not enclosed by '\' inside strings
|
changeset |
files
|
| Mon, 14 Nov 1994 14:29:20 +0100 |
clasohm |
updated remarks about grammar; added section about ambiguities
|
changeset |
files
|
| Mon, 14 Nov 1994 11:57:32 +0100 |
wenzelm |
exported 'cat';
|
changeset |
files
|
| Mon, 14 Nov 1994 10:49:39 +0100 |
lcp |
Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of:
|
changeset |
files
|