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.
instantiate: omit has_duplicates check, which is irrelevant for soundness;
20060915, by wenzelm
trivial whitespace change
20060915, by webertj
tuned;
20060915, by wenzelm
more on theorems;
20060914, by wenzelm
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
20060914, by huffman
add instance for class division_ring
20060914, by huffman
removed duplicate lemmas
20060914, by huffman
fixed syntax clash with Real/RealVector
20060914, by huffman
*** empty log message ***
20060914, by wenzelm
Function package: Outside their domain functions now return "arbitrary".
20060914, by krauss
updated makefile
20060914, by krauss
Fixed Subscript Exception occurring with HigherOrder recursion
20060914, by krauss
remove conflicting norm syntax
20060914, by huffman
made SML/NJ happy;
20060914, by wenzelm
added exists_type;
20060913, by wenzelm
renamed NameSpace.drop_base to NameSpace.qualifier;
20060913, by wenzelm
Updated keyword file
20060913, by krauss
Removed debugging code imports...
20060913, by krauss
Added the "theory_const" option. Only it is OFF because it's often harmful!
20060913, by paulson
Extended the blacklist with higherorder theorems. Restructured. Added checks to
20060913, by paulson
bug fix to abstractions: free variables in theorem can be abstracted over.
20060913, by paulson
Tweaks to is_fol_term, the firstorder test. We don't count "=" as a connective
20060913, by paulson
Major update to function package, including new syntax and the (only theoretical)
20060913, by krauss
added instance rat :: recpower
20060913, by huffman
more on theorems;
20060912, by wenzelm
tuned;
20060912, by wenzelm
more on terms;
20060912, by wenzelm
no_syntax norm  clash with Real/RealVector.thy;
20060912, by wenzelm
simplify some proofs, remove obsolete realpow_divide
20060912, by huffman
realpow_divide > power_divide
20060912, by huffman
remove extra dependency
20060912, by huffman
more on terms;
20060912, by wenzelm
Efficient term substitution  avoids copying.
20060912, by wenzelm
ctyp: maintain maxidx;
20060912, by wenzelm
removed obsolete aconvs (use eq_list aconv);
20060912, by wenzelm
tuned eq_list;
20060912, by wenzelm
moved term subst functions to TermSubst;
20060912, by wenzelm
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
20060912, by wenzelm
added Pure/term_subst.ML;
20060912, by wenzelm
added Gentzen:1935;
20060912, by wenzelm
import RealVector
20060912, by huffman
formalization of vector spaces and algebras over the real numbers
20060912, by huffman
induct method: renamed 'fixing' to 'arbitrary';
20060911, by wenzelm
updated;
20060911, by wenzelm
more rules;
20060911, by wenzelm
hid succ, pred in Numeral.thy
20060911, by haftmann
updated;
20060911, by wenzelm
more rules;
20060911, by wenzelm
tuned;
20060911, by wenzelm
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
20060910, by huffman
cleaned up
20060909, by huffman
tuned;
20060908, by wenzelm
tuned;
20060908, by wenzelm
changed order of type classes and axclasses
20060908, by haftmann
tuned;
20060907, by wenzelm
updated;
20060907, by wenzelm
tentative appendix C;
20060907, by wenzelm
tuned;
20060907, by wenzelm
read_instantiate: declare names of TVars as well (temporary workaround for nofreeze feature of type inference);
20060906, by wenzelm
rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list
20060906, by webertj
less
more

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