Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
1000
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.
Indexing of FILTER and COND
19950511, by lcp
show_sorts
19950511, by lcp
Modified translation for pattern abstraction.
19950510, by nipkow
Moved induct2 from Hoare to Lfp.
19950509, by nipkow
Prod is now a parent of Lfp.
19950509, by nipkow
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
19950509, by clasohm
added \CHOL
19950509, by clasohm
Calls 'rail' program for syntax diagrams
19950504, by lcp
Changed some definitions and proofs to use patternmatching.
19950504, by lcp
Changed to use split instead of fsplit. The weakening of fsplitE appears not
19950504, by lcp
case is defined using patternmatching
19950504, by lcp
Modified proofs for new form of 'split'.
19950504, by lcp
Added patternmatching code from CHOL/Prod.thy. Changed
19950504, by lcp
Modified proofs for (q)split, fst, snd for new
19950503, by lcp
Changed to use split instead of fsplit. The weakening of fsplitE appears not
19950503, by lcp
prove_case_equation now calls uses meta_eq_to_obj_eq to cope
19950503, by lcp
show_sorts:=true forces display of types
19950503, by lcp
trivial rewording
19950503, by lcp
trivial change
19950503, by lcp
Covers wrapper tacticals: setwrapper, ..., addss
19950503, by lcp
fixed bug in thy_unchanged that occurred when the .thy file was changed
19950503, by clasohm
Changed definitions so that qsplit is now defined in terms of
19950503, by lcp
Modified proofs for (q)split, fst, snd for new
19950503, by lcp
Changed some definitions and proofs to use patternmatching.
19950503, by lcp
Patterns can now be letbound
19950503, by lcp
Changed to use split instead of fsplit. The weakening of fsplitE appears not
19950503, by lcp
Changed some definitions and proofs to use patternmatching.
19950503, by lcp
Changed some definitions and proofs to use patternmatching.
19950503, by lcp
Changed some definitions and proofs to use patternmatching.
19950503, by lcp
Now show_sorts:=true causes printing of types
19950503, by lcp
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
19950503, by lcp
replaced store_thm by bind_thm
19950503, by clasohm
trivial change
19950503, by lcp
new version
19950503, by lcp
Covers defs and reordering of theory sections
19950503, by lcp
Updates involving defs, addss, etc.
19950503, by lcp
Simplified layout a little.
19950503, by nipkow
Corrected display of split f t: no more let.
19950503, by nipkow
Sections can now be given in any order.
19950502, by nipkow
Simplified proof of Hausdorff_next_exists.
19950501, by lcp
Added
19950428, by nipkow
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
19950428, by lcp
Modified proofs for new claset primitives. The problem is that they enforce
19950428, by lcp
Modified proofs for new claset primitives. The problem is that they enforce
19950428, by lcp
Modified proofs for new claset primitives. The problem is that they enforce
19950428, by lcp
Recoded addSIs, etc., so that nets are built incrementally
19950428, by lcp
updated version
Isabelle943
19950425, by lcp
Simple updates for compatibility with KG
19950425, by lcp
Simplified, removing needless theorems about lambda.
19950425, by lcp
Now loads the theory "Let". Could add it to FOL, but this appears to
19950425, by lcp
HOL.thy:
19950422, by nipkow
I have modified the grammar for idts (sequences of identifiers with optional
19950422, by nipkow
Simplified proofs thanks to addss.
19950419, by nipkow
Fixed old bug in the simplifier. Term to be simplified now carries around its
19950416, by nipkow
Fixed bug.
19950416, by nipkow
Brought in line with new organization of IOA.
19950416, by nipkow
New examples directories Resid and AC
19950414, by lcp
Definition of 'let' declarations, from HOL
19950414, by lcp
In binders, the default body priority is now p instead of 0.
19950414, by lcp
Now builds Resid as a test
19950414, by lcp
less
more

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