Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
120
+120
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
le_imp_lepoll: renamed to Card_le_imp_lepoll
19941208, by lcp
Card_cardinal_le: new
19941208, by lcp
changed Pure's grammar and the way types are converted to nonterminals
19941208, by clasohm
replaced type_syn by pure_syn in Pure signature
19941208, by clasohm
test_assume_tac: now tries eq_assume_tac on exceptional cases
19941208, by lcp
res_inst_tac: added comments
19941208, by lcp
added qed and qed_goal[w]
19941207, by clasohm
moved first call of store_theory from thy_read.ML to created .thy.ML file
19941207, by clasohm
added bind_thm
19941206, by clasohm
added qed and qed_goal[w]
19941130, by clasohm
added qed_goal for meta_iffD
19941130, by clasohm
replaced "val ... = result()" by "qed ..."
19941130, by clasohm
le_UN_Ord_lt_csucc: added comment
19941129, by lcp
replaced "rules" by "defs"
19941129, by lcp

19941128, by regensbu
ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any
19941125, by lcp
checks that the recursive sets are Consts before taking
19941125, by lcp
equiv_comp_eq: simplified proof
19941125, by lcp
moved Cantors theorem here from ZF/ex/misc
19941125, by lcp
deepen_tac: modified due to outcome of experiments. Its
19941125, by lcp
added qed_goal[w]
19941125, by clasohm
added blank line
19941125, by lcp
tidied proofs, using fast_tac etc. as much as possible
19941125, by lcp
prove_fun: new; no longer depends upon the version in simpdata.ML
19941125, by lcp
data_domain,Codata_domain: removed replicate; now return one
19941124, by lcp
tidied proofs, using fast_tac etc. as much as possible
19941124, by lcp
added comments on alternative uses of type_intrs/elims
19941124, by lcp
modified for new treatment of mutual recursion
19941124, by lcp
the_equality: more careful use of addSIs and addIs
19941124, by lcp
cons_fun_eq: modified strange uses of classical reasoner
19941124, by lcp
moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML
19941124, by lcp
moved version of Cantors theorem to ZF/Perm.ML
19941124, by lcp
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
19941124, by lcp
ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
19941124, by lcp
updated for new deepen_tac
19941124, by lcp
trivial changes
19941124, by lcp
new reference to HO patterns
19941123, by lcp
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
19941122, by lcp
Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars
19941122, by lcp
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
19941121, by lcp
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
19941121, by lcp
replaced 'val ... = result();' by 'qed "...";'
19941121, by clasohm
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
19941121, by lcp
ZF/EquivClass/congruent_commuteI: uncommented and simplified proof
19941121, by lcp
ZF/ZF.ML/UN_iff, INT_iff: added to the signature
19941121, by lcp
Pure/thm/norm_term_skip: new, for skipping normalization of the context
19941121, by lcp
Pure/sequence: added comment explaining that memoing sequences were found
19941121, by lcp
Pure/envir/norm_term: replaced equality test for [] by null
19941121, by lcp
page 157 erratum
19941121, by lcp
now searches all subdirectories of objectlogics
19941121, by lcp
Chnaged simplifier description (lhss)
19941118, by nipkow
added call of store_theory after thy file has been read
19941118, by clasohm
Updated description of valid lhss.
19941118, by nipkow
In ZF, type i has class term, not (just) logic
19941117, by lcp
added check for newlines not enclosed by '\' inside strings
19941114, by clasohm
updated remarks about grammar; added section about ambiguities
19941114, by clasohm
exported 'cat';
19941114, by wenzelm
Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of:
19941114, by lcp
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
19941114, by lcp
Added month for Coens thesis
19941114, by lcp
removal of FOL_dup_cs
19941111, by lcp
removal of HOL_dup_cs
19941111, by lcp
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
19941111, by lcp
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
19941111, by lcp
FOL/intprover/safe_tac: now uses REPEAT_DETERM_FIRST instead of REPEAT_DETERM
19941111, by lcp
argument swaps in HOL
19941111, by lcp
HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
19941110, by lcp
updated pathnames
19941110, by lcp
updated discussion of congruence rules in first section
19941109, by lcp
changed warning for extremely ambiguous expressions
19941109, by clasohm
Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
19941103, by lcp
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
19941103, by lcp
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
19941103, by lcp
ZF/Perm/inj_converse_fun: tidied; removed uses of PiI/E
19941103, by lcp
ZF/InfDatatype/fun_Vcsucc: removed use of PiE
19941103, by lcp
ZF/func: tidied many proofs, using new definition of Pi(A,B)
19941103, by lcp
ZF: NEW DEFINITION OF PI(A,B)
19941103, by lcp
ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
19941103, by lcp
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
19941103, by lcp
ZF/domrange/converse_iff: new
19941103, by lcp
ZF/upair/theI2: new
19941103, by lcp
ZF/equalities/domain_converse,range_converse,
19941103, by lcp
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
19941103, by lcp
Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
19941103, by lcp
added warning message
19941103, by clasohm
Provers/classical: now takes theorem "classical" as argument, proves "swap"
19941102, by lcp
Provers/hypsubst: greatly simplified! No longer simulates a
19941102, by lcp
Pure/sign/infer_types/exn_type_msg: new, for more uniform handling of
19941102, by lcp
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
19941102, by nipkow
FOL/FOL/swap: deleted
19941101, by lcp
HOLCF/Ssum3.ML: changed res_inst_tac [("P"... to res_inst_tac [("Pa" in
19941101, by lcp
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
19941031, by lcp
ZF/domrange/image_subset: tidied
19941031, by lcp
ZF/upair/mem_asym,succ_inject: tidied
19941031, by lcp
com1,2: added simplifier calls to remove use of ssubst in fast_tac
19941031, by lcp
Pure/tctical/THEN_ELSE: new
19941031, by lcp
Pure/tactic/build_netpair: now takes two arguments
19941031, by lcp
Pure/sequence/hd,tl: new
19941031, by lcp
Pure/drule/thin_rl: new
19941031, by lcp
FOL/ex/ROOT: now loads mini.ML
19941031, by lcp
FOL/ROOT/FOL_dup_cs: removed as obsolete
19941031, by lcp
FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
19941031, by lcp
ZF/ZF/ex1_functional: moved to FOL/ROOT
19941031, by lcp
Miniscope conversoin; example of formula rewriting
19941031, by lcp
ZF/OrderArith/thin: deleted as obsolete
19941031, by lcp
added final newline
19941031, by lcp
added header files; deleted commentedout code
19941031, by lcp
Prepared the code for preservation of bound var names during rewriting. Still
19941028, by nipkow
removed superfluous type_intrs in datatype com.
19941026, by nipkow
simplified syntax of infix continuous functiuons
19941026, by nipkow
strip_quotes now exported;
19941025, by wenzelm
minor change of occs_const in dest_defn;
19941025, by wenzelm
added require_thy;
19941025, by wenzelm
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
19941024, by lcp
ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
19941021, by lcp
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
19941021, by lcp
LK/hardquant/37: deleted call to flexflex_tac: no longer needed
19941021, by lcp
LCF/LCF.thy: the constant VOID had mixfix syntax "()" !! Added quotes.
19941021, by lcp
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
19941021, by lcp
ZF/Fixedpt/coinduct: modified proof to suppress deep unification
19941019, by lcp
less
more

(0)
120
+120
+1000
+3000
+10000
+30000
tip