| Thu, 15 Dec 1994 11:08:22 +0100 |
lcp |
qconverse_qconverse, qconverse_prod: renamed from
|
changeset |
files
|
| Wed, 14 Dec 1994 17:24:23 +0100 |
lcp |
well_ord_iso_predE replaces not_well_ord_iso_pred
|
changeset |
files
|
| Wed, 14 Dec 1994 17:15:54 +0100 |
lcp |
Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of
|
changeset |
files
|
| Wed, 14 Dec 1994 16:57:55 +0100 |
lcp |
converse_UN, Diff_eq_0_iff: new
|
changeset |
files
|
| Wed, 14 Dec 1994 16:54:13 +0100 |
lcp |
added constants mono_map, ord_iso_map
|
changeset |
files
|
| Wed, 14 Dec 1994 16:51:16 +0100 |
lcp |
cardinal_UN_Ord_lt_csucc: added comment
|
changeset |
files
|
| Wed, 14 Dec 1994 16:48:36 +0100 |
lcp |
conj_commute,disj_commute: new
|
changeset |
files
|
| Wed, 14 Dec 1994 13:03:09 +0100 |
clasohm |
changed get_thm to search all parent theories if the theorem is not found
|
changeset |
files
|
| Wed, 14 Dec 1994 11:41:49 +0100 |
clasohm |
added bind_thm for theorems defined by "standard ..."
|
changeset |
files
|
| Wed, 14 Dec 1994 10:26:30 +0100 |
wenzelm |
added any, sprop to pure_types;
|
changeset |
files
|
| Wed, 14 Dec 1994 10:24:54 +0100 |
wenzelm |
removed "logic1";
|
changeset |
files
|
| Tue, 13 Dec 1994 11:51:12 +0100 |
clasohm |
removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
|
changeset |
files
|
| Mon, 12 Dec 1994 10:26:05 +0100 |
wenzelm |
added print_theory that prints stored thms;
|
changeset |
files
|
| Fri, 09 Dec 1994 16:44:31 +0100 |
wenzelm |
minor internal changes;
|
changeset |
files
|
| Fri, 09 Dec 1994 16:42:09 +0100 |
wenzelm |
improved axioms_of: returns thms as the manual says;
|
changeset |
files
|
| Fri, 09 Dec 1994 13:39:52 +0100 |
clasohm |
removed ZF_Lemmas and added qed_goal
|
changeset |
files
|
| Fri, 09 Dec 1994 13:05:03 +0100 |
clasohm |
added warning for already stored theorem to store_thm
|
changeset |
files
|
| Thu, 08 Dec 1994 16:42:58 +0100 |
lcp |
sum_ss: moved down and added the rewrite rules for "case"
|
changeset |
files
|
| Thu, 08 Dec 1994 16:07:12 +0100 |
lcp |
leI: added comment
|
changeset |
files
|
| Thu, 08 Dec 1994 15:37:28 +0100 |
lcp |
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
|
changeset |
files
|
| Thu, 08 Dec 1994 15:07:48 +0100 |
lcp |
sum_ss: deleted because it conflicts with the one in Sum.ML
|
changeset |
files
|
| Thu, 08 Dec 1994 14:38:58 +0100 |
lcp |
not_well_ord_iso_pred: removed needless quantifier
|
changeset |
files
|
| 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
|
| Mon, 14 Nov 1994 10:46:50 +0100 |
lcp |
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
|
changeset |
files
|
| Mon, 14 Nov 1994 10:41:25 +0100 |
lcp |
Added month for Coens thesis
|
changeset |
files
|
| Fri, 11 Nov 1994 10:53:41 +0100 |
lcp |
removal of FOL_dup_cs
|
changeset |
files
|
| Fri, 11 Nov 1994 10:50:49 +0100 |
lcp |
removal of HOL_dup_cs
|
changeset |
files
|
| Fri, 11 Nov 1994 10:42:55 +0100 |
lcp |
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
|
changeset |
files
|
| Fri, 11 Nov 1994 10:41:09 +0100 |
lcp |
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
|
changeset |
files
|
| Fri, 11 Nov 1994 10:33:05 +0100 |
lcp |
FOL/intprover/safe_tac: now uses REPEAT_DETERM_FIRST instead of REPEAT_DETERM
|
changeset |
files
|
| Fri, 11 Nov 1994 10:31:51 +0100 |
lcp |
argument swaps in HOL
|
changeset |
files
|
| Thu, 10 Nov 1994 11:36:40 +0100 |
lcp |
HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
|
changeset |
files
|
| Thu, 10 Nov 1994 11:06:44 +0100 |
lcp |
updated pathnames
|
changeset |
files
|
| Wed, 09 Nov 1994 15:47:11 +0100 |
lcp |
updated discussion of congruence rules in first section
|
changeset |
files
|
| Wed, 09 Nov 1994 13:50:59 +0100 |
clasohm |
changed warning for extremely ambiguous expressions
|
changeset |
files
|
| Thu, 03 Nov 1994 16:52:19 +0100 |
lcp |
Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
|
changeset |
files
|
| Thu, 03 Nov 1994 16:39:41 +0100 |
lcp |
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
|
changeset |
files
|
| Thu, 03 Nov 1994 16:05:22 +0100 |
lcp |
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
|
changeset |
files
|
| Thu, 03 Nov 1994 13:42:39 +0100 |
lcp |
ZF/Perm/inj_converse_fun: tidied; removed uses of PiI/E
|
changeset |
files
|
| Thu, 03 Nov 1994 12:43:42 +0100 |
lcp |
ZF/InfDatatype/fun_Vcsucc: removed use of PiE
|
changeset |
files
|
| Thu, 03 Nov 1994 12:39:39 +0100 |
lcp |
ZF/func: tidied many proofs, using new definition of Pi(A,B)
|
changeset |
files
|
| Thu, 03 Nov 1994 12:35:41 +0100 |
lcp |
ZF: NEW DEFINITION OF PI(A,B)
|
changeset |
files
|
| Thu, 03 Nov 1994 12:30:55 +0100 |
lcp |
ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
|
changeset |
files
|
| Thu, 03 Nov 1994 12:26:59 +0100 |
lcp |
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
|
changeset |
files
|
| Thu, 03 Nov 1994 12:23:19 +0100 |
lcp |
ZF/domrange/converse_iff: new
|
changeset |
files
|
| Thu, 03 Nov 1994 12:06:37 +0100 |
lcp |
ZF/upair/theI2: new
|
changeset |
files
|
| Thu, 03 Nov 1994 11:58:16 +0100 |
lcp |
ZF/equalities/domain_converse,range_converse,
|
changeset |
files
|
| Thu, 03 Nov 1994 11:52:04 +0100 |
lcp |
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
|
changeset |
files
|
| Thu, 03 Nov 1994 11:45:41 +0100 |
lcp |
Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
|
changeset |
files
|
| Thu, 03 Nov 1994 08:34:53 +0100 |
clasohm |
added warning message
|
changeset |
files
|
| Wed, 02 Nov 1994 12:48:22 +0100 |
lcp |
Provers/classical: now takes theorem "classical" as argument, proves "swap"
|
changeset |
files
|
| Wed, 02 Nov 1994 12:44:03 +0100 |
lcp |
Provers/hypsubst: greatly simplified! No longer simulates a
|
changeset |
files
|
| Wed, 02 Nov 1994 10:45:14 +0100 |
lcp |
Pure/sign/infer_types/exn_type_msg: new, for more uniform handling of
|
changeset |
files
|
| Wed, 02 Nov 1994 09:09:30 +0100 |
nipkow |
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
|
changeset |
files
|
| Tue, 01 Nov 1994 10:40:10 +0100 |
lcp |
FOL/FOL/swap: deleted
|
changeset |
files
|
| Tue, 01 Nov 1994 10:32:18 +0100 |
lcp |
HOLCF/Ssum3.ML: changed res_inst_tac [("P"... to res_inst_tac [("Pa" in
|
changeset |
files
|
| Mon, 31 Oct 1994 18:15:24 +0100 |
lcp |
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
|
changeset |
files
|
| Mon, 31 Oct 1994 18:11:12 +0100 |
lcp |
ZF/domrange/image_subset: tidied
|
changeset |
files
|
| Mon, 31 Oct 1994 18:09:32 +0100 |
lcp |
ZF/upair/mem_asym,succ_inject: tidied
|
changeset |
files
|
| Mon, 31 Oct 1994 18:07:29 +0100 |
lcp |
com1,2: added simplifier calls to remove use of ssubst in fast_tac
|
changeset |
files
|
| Mon, 31 Oct 1994 18:03:14 +0100 |
lcp |
Pure/tctical/THEN_ELSE: new
|
changeset |
files
|