Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
10000
3000
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.
added lattice_locales
20050209, by nipkow
Extracted generic lattice stuff to new Lattice_Locales.thy
20050209, by nipkow
New
20050209, by nipkow
new foldSet proofs
20050209, by paulson
revised fold1 proofs
20050209, by paulson
revised fold1 proofs
20050209, by paulson
cvs merge problem fixed
20050208, by nipkow
new treatment of fold1
20050208, by paulson
Fixed lattice defns
20050208, by nipkow
*** empty log message ***
20050207, by nipkow
fixed latex problems by including bigsqcap
20050207, by nipkow
fixed latex problems
20050207, by nipkow
fixed mac line
20050206, by paulson
Added Lattice locale
20050205, by nipkow
clausification and proof reconstruction
20050204, by paulson
comment
20050204, by paulson
Added semilattice locales and reorganized fold1 lemmas
20050204, by nipkow
added find_rewrites
20050203, by nipkow
new treatment of demodulation in proof reconstruction
20050203, by paulson
don't generate latex for LaTeXsugar and OptionalSugar
20050203, by kleing
removed sugar.sty (obsolete for devel version)
20050203, by kleing
not needed any more by LaTeXSugar
20050203, by kleing
Document now applies to devel version (and Isabelle 2005)
20050203, by kleing
Replaced application of subst by simplesubst in proof of app_Var_NF
20050202, by berghofe
Replaced application of subst by simplesubst in proof of rev_induct
20050202, by berghofe
tidying of some subst/simplesubst proofs
20050202, by paulson
generalization and tidying
20050202, by paulson
improved handling of chained facts
20050202, by paulson
Max_le > Max_ge
20050202, by nipkow
fold and fol1 changes
20050202, by nipkow
added [simp]
20050202, by nipkow
link to PG FAQ for start up problem
20050202, by kleing
the new subst tactic, by Lucas Dixon
20050201, by paulson
renamed a few vars, added a lemma
20050130, by nipkow
proof simpification
20050128, by nipkow
moved sugar.sty to textinputs
20050128, by kleing
H false for showing proofs (not H true)
20050128, by kleing
fixed bugs
20050127, by nipkow
 Proofs are now hidden by default when generating documents
20050127, by berghofe
Proofs are now hidden by default.
20050127, by berghofe
 Proofs are now hidden by default
20050127, by berghofe
Added show_var_qmarks flag.
20050127, by berghofe
*** empty log message ***
20050126, by nipkow
added OptionalSugar
20050126, by nipkow
new
20050126, by nipkow
moved to HOL/Library
20050126, by nipkow
*** empty log message ***
20050126, by nipkow
implemented cache for conversion to clauses
20050126, by paulson
enclosed in (*<*) (*>*)
20050125, by nipkow
Added variant of eres_inst_tac that operates on indexnames instead of strings.
20050124, by berghofe
Adapted to modified interface of PureThy.get_thm(s).
20050124, by berghofe
Eliminated hack for deleting leading question mark from induction
20050124, by berghofe
Replaced xstring by thmref.
20050124, by berghofe
Removed unnecessary subsignature checks to speed up rewriting.
20050124, by berghofe
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
20050124, by berghofe
Replaced xstring by thmref.
20050124, by berghofe
Adapted to modified interface of PureThy.get_thm(s).
20050124, by berghofe
Specific theorems in a named list of theorems can now be referred to
20050124, by berghofe
updated description of arith_tac
20050124, by paulson
thin_tac now works on P==>Q
20050124, by paulson
less
more

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