Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
300
100
60
+60
+100
+300
+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.
deleted obsolete references to ISABELLEMAKE
19940819, by lcp
/unvarifyT, unvarify: moved to Pure/logic.ML
19940818, by lcp
Pure/goals.ML: prove_goalw_cterm now does its own exceptionhandling, moved
19940818, by lcp
Pure/library/assert_all: new, moved from ZF/ind_syntax.ML
19940818, by lcp
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
19940818, by lcp
HOLCF/Lift1.thy: updated for new sum_case by using "case" syntax
19940818, by lcp
overheads for inductive definitions, originally for CADE12
19940817, by lcp
ZF/ex/ROOT: added .ML to use command use "ex/twos_compl"
19940817, by lcp
ZF/ex/Ntree: two new examples, maptree and maptree2
19940817, by lcp
ZF/func/fun_extend3: new
19940817, by lcp
ZF/Univ/Sigma_subset_univ, Transset_Pair_subset_univ: deleted
19940817, by lcp
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
19940816, by lcp
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
19940816, by lcp
ZF/Finite: added the finite function space, A>B
19940816, by lcp
ZF/pair.ML: moved some definitions here from simpdata.ML
19940816, by lcp
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
19940816, by lcp
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
19940816, by lcp
ZF/Makefile/FILES: added many missing .thy files
19940815, by lcp
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
19940815, by lcp
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
19940815, by lcp
ZF/ex/CoUnit/lleq_cs: copied from LList.ML
19940815, by lcp
ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit;
19940815, by lcp
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
19940815, by lcp
ZF/InfDatatype: simplified, extended results for infinite branching
19940815, by lcp
ZF/CardinalArith/InfCard_Un: new
19940815, by lcp
ZF/Cardinal/Card_Un: new
19940815, by lcp
ZF/Sum/Sigma_bool: new
19940815, by lcp
ZF/equalities/Sigma_cons: new
19940815, by lcp
ZF/func/empty_fun: renamed from fun_empty
19940815, by lcp
Proof beautification
19940815, by nipkow
for infinite datatypes with arbitrary index sets
19940812, by lcp
installation of new inductive/datatype sections
19940812, by lcp
installation of new inductive/datatype sections
19940812, by lcp
addition of string escapes
19940812, by lcp
updated reference to parents
19940812, by lcp
Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents
19940812, by lcp
reorganized using new theory sections
19940812, by lcp
Simplified some proofs. Added some type assumptions to the introduction rules.
19940808, by nipkow
fixed spelling
19940804, by lcp
addition of show_brackets
19940804, by lcp
addition of show_brackets
19940804, by lcp
improved show_brackets again  Trueprop does not create () any more.
19940803, by nipkow
minimized () in forced printing of barckets (show_brackets)
19940802, by nipkow
added flag show_brackets for printinmg fully bracketed terms.
19940802, by nipkow
trivial whitespace change
19940801, by lcp
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
19940801, by lcp
ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical
19940729, by lcp
some small simplifications
19940729, by nipkow
deleted repeated "the" in "before the the .thy file"
19940729, by lcp
renamed union_iff to Union_iff
19940729, by lcp
revised for new theory system: removal of ext, addition of thy_name
19940729, by lcp
Inductive defs need no longer mention SigmaI/E2
19940729, by lcp
ZF/intr_elim/intro_tacsf: now uses SigmaI as a default intro rule and
19940729, by lcp
ZF/WF/wf_induct: streamlined proof
19940728, by lcp
ZF/constructor.thy: now specifies intr_elim as its parent; previously had
19940728, by lcp
added a new example due to Robin Arthan
19940727, by lcp
logics update
19940727, by lcp
Addition of infinite branching datatypes
19940727, by lcp
Addition of infinite branching datatypes
19940727, by lcp
Addition of infinite branching datatypes
19940727, by lcp
less
more

(0)
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip