Mercurial
Mercurial
>
repos
>
isabelle
/ shortlog
summary
| shortlog |
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
(0)
-10000
-3000
-1000
-300
-100
-30
-10
-7
+7
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Sun, 17 Jun 2007 18:47:03 +0200
nipkow
tuned laws for cancellation in divisions for fields.
changeset
|
files
Sun, 17 Jun 2007 13:39:50 +0200
chaieb
moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs
changeset
|
files
Sun, 17 Jun 2007 13:39:48 +0200
chaieb
Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
changeset
|
files
Sun, 17 Jun 2007 13:39:45 +0200
chaieb
gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f;
changeset
|
files
Sun, 17 Jun 2007 13:39:39 +0200
chaieb
thin_prems_tac first max-scopes universal quantifiers; eta_conv moved to Pure/conv.ML
changeset
|
files
Sun, 17 Jun 2007 13:39:34 +0200
chaieb
Tuned error messages; tuned;
changeset
|
files
Sun, 17 Jun 2007 13:39:32 +0200
chaieb
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
changeset
|
files
(0)
-10000
-3000
-1000
-300
-100
-30
-10
-7
+7
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip