Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
300
100
50
30
+30
+50
+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.
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
less
more

(0)
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip