Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-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 JavaScript-enabled browsers.
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
1998-03-09, by wenzelm
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
1998-03-09, by wenzelm
Removed `addsplits [expand_if]'
1998-03-07, by nipkow
added clasimp.ML;
1998-03-06, by wenzelm
Removed superfluous `op'
1998-03-06, by nipkow
*** empty log message ***
1998-03-06, by nipkow
Added delspilts, Addsplits, Delsplits.
1998-03-06, by nipkow
expand_if is now by default part of the simpset.
1998-03-06, by nipkow
New theorem and simprules
1998-03-05, by paulson
Reorganized simplifier. May now reorient rules.
1998-03-04, by nipkow
Reorganized simplifier. May now reorient rules.
1998-03-04, by nipkow
Reorganized simplifier. May now reorient rules.
1998-03-04, by nipkow
Better simplification allows deletion of parts of proofs
1998-03-03, by paulson
New theorem
1998-03-03, by paulson
New theorems
1998-03-03, by paulson
New theorems; tidied
1998-03-03, by paulson
New theorem diff_Suc_le_Suc_diff; tidied another proof
1998-03-03, by paulson
auto generated
1998-03-03, by paulson
Modified def.
1998-02-28, by nipkow
Splitters via named loopers.
1998-02-28, by nipkow
Little reorganization. Loop tactics have names now.
1998-02-28, by nipkow
Tried to reorganize rewriter a little. More to be done.
1998-02-28, by nipkow
added minimal description of rep_cs: corrections
1998-02-27, by oheimb
added minimal description of rep_cs
1998-02-27, by oheimb
added minimal description of rep_ss
1998-02-27, by oheimb
"choice" moved to Set.ML
1998-02-27, by paulson
New absorbsion laws, etc
1998-02-27, by paulson
Vimage
1998-02-27, by paulson
New vimage laws
1998-02-27, by paulson
added smart_tac
1998-02-26, by oheimb
removed superfluous addss
1998-02-26, by oheimb
New theory, Vimage
1998-02-26, by paulson
Proved choice and bchoice; changed Fun.thy -> thy
1998-02-26, by paulson
*** empty log message ***
1998-02-26, by wenzelm
added clasimp.ML;
1998-02-26, by wenzelm
renamed rep_claset to rep_cs
1998-02-25, by oheimb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
1998-02-25, by oheimb
changed wrapper mechanism of classical reasoner
1998-02-25, by oheimb
added split_all_tac to claset()
1998-02-25, by oheimb
changed wrapper mechanism of classical reasoner
1998-02-25, by oheimb
New theory of the inverse image of a function
1998-02-24, by paulson
Added some lemmas.
1998-02-24, by nipkow
Catches bad elim rules, handling exception OPTION
1998-02-23, by paulson
New laws for union
1998-02-23, by paulson
New laws for id
1998-02-23, by paulson
New induction schemas for lists (length and snoc).
1998-02-22, by nipkow
*** empty log message ***
1998-02-20, by nipkow
Congruence rules use == in premises now.
1998-02-20, by nipkow
Congruence rules use == in premises now.
1998-02-20, by nipkow
minor improvements
1998-02-20, by oheimb
re-arranged bindings for many function keys
1998-02-20, by oheimb
extended input syntax to handle names of special keys
1998-02-20, by oheimb
moved Ctrl entry before Alt entry
1998-02-20, by oheimb
New theorem eq_imp_le
1998-02-20, by paulson
Four new Union/Intersection laws
1998-02-19, by paulson
corrected problem with auto_tac: now uses a variant of depth_tac that avoids
1998-02-18, by oheimb
added New Jersey mirror;
1998-02-18, by wenzelm
Improved loop-test for rewrite rules a little.
1998-02-18, by nipkow
tuned comment;
1998-02-18, by wenzelm
added append (curried);
1998-02-13, by wenzelm
less
more
|
(0)
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip