Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+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.
Poly/ML startup script (for 4.9.1);
2006-09-27, by wenzelm
added ML-Systems/polyml-4.9.1.ML;
2006-09-27, by wenzelm
Compatibility wrapper for Poly/ML 4.9.1.
2006-09-27, by wenzelm
removed all references to star_n and FreeUltrafilterNat
2006-09-27, by huffman
add lemmas about hnorm, Infinitesimal
2006-09-27, by huffman
reverted to 1.58;
2006-09-27, by wenzelm
proper const_syntax for uminus, abs;
2006-09-27, by wenzelm
reorganized HNatInfinite proofs; simplified and renamed some lemmas
2006-09-27, by huffman
removed obsolete of_instream_slurp -- now already included in tty;
2006-09-27, by wenzelm
Source.tty now slurps by default;
2006-09-27, by wenzelm
of_stream/tty: slurp input eagerly;
2006-09-27, by wenzelm
tuned all_paths;
2006-09-27, by wenzelm
internal params: Vartab instead of AList;
2006-09-27, by wenzelm
removed unused serial_of, name_of;
2006-09-27, by wenzelm
removed redundant lemmas;
2006-09-27, by wenzelm
remove redundant lemmas
2006-09-27, by huffman
replaced constant 0 by HOL.zero
2006-09-27, by haftmann
hypreal_of_nat abbreviates of_nat
2006-09-27, by huffman
add lemmas of_real_eq_star_of, Reals_eq_Standard
2006-09-27, by huffman
move star_of_norm from SEQ.thy to NSA.thy
2006-09-27, by huffman
convert more proofs to transfer principle
2006-09-27, by huffman
add lemmas about Standard, real_of, scaleR
2006-09-27, by huffman
instance complex :: real_normed_field; cleaned up
2006-09-27, by huffman
add lemma stc_unique; shorten stc proofs
2006-09-27, by huffman
add lemmas approx_diff and st_unique, shorten st proofs
2006-09-27, by huffman
add lemmas about of_real and power
2006-09-27, by huffman
reorganize section headings
2006-09-27, by huffman
more lemmas about Standard and star_of
2006-09-27, by huffman
define new constant Standard = range star_of
2006-09-27, by huffman
add lemmas of_int_in_Reals, of_nat_in_Reals
2006-09-27, by huffman
add header
2006-09-26, by huffman
Changed precedence of "op O" (relation composition) from 60 to 75.
2006-09-26, by krauss
handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype
2006-09-26, by haftmann
tuned syntax for <= <
2006-09-26, by haftmann
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-26, by haftmann
renamed 0 and 1 to HOL.zero and HOL.one respectivly
2006-09-26, by haftmann
fixed the definition of "depth"
2006-09-26, by paulson
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
2006-09-26, by paulson
some cleanup
2006-09-25, by haftmann
changed order
2006-09-25, by haftmann
inserted headings
2006-09-25, by haftmann
changed interface in codegen_package.ML
2006-09-25, by haftmann
fixed some mess
2006-09-25, by haftmann
cleaned up
2006-09-25, by haftmann
adding constants the modern way
2006-09-25, by haftmann
added examples for variable name handling
2006-09-25, by haftmann
better handling for div by zero
2006-09-25, by haftmann
updated theory description
2006-09-25, by haftmann
refinements in codegen serializer
2006-09-25, by haftmann
added 'undefined' serializer
2006-09-25, by haftmann
added code_instname
2006-09-25, by haftmann
reorganized subsection headings
2006-09-24, by huffman
moved SEQ_Infinitesimal from SEQ to HyperNat
2006-09-24, by huffman
real_norm_def [simp]
2006-09-24, by huffman
generalize types of lim and nslim
2006-09-24, by huffman
generalized types of sums, summable, and suminf
2006-09-24, by huffman
add lemma convergent_Cauchy
2006-09-24, by huffman
remove extra dependencies
2006-09-24, by huffman
add proof of summable_LIMSEQ_zero
2006-09-24, by huffman
change definitions from SOME to THE
2006-09-24, by huffman
move root and sqrt stuff from Transcendental to NthRoot
2006-09-24, by huffman
fix proof
2006-09-24, by huffman
added lemmas about LIMSEQ and norm; simplified some proofs
2006-09-22, by huffman
add lemma norm_power
2006-09-22, by huffman
added HOL-Complex-ex;
2006-09-22, by wenzelm
define constants with THE instead of SOME
2006-09-22, by huffman
Fixed bug concerning the generation of identifiers for
2006-09-22, by berghofe
Replaced irreducible_paths by all_paths.
2006-09-22, by berghofe
Added function all_paths (formerly find_paths).
2006-09-22, by berghofe
tuned proofs;
2006-09-22, by wenzelm
tuned oracle name;
2006-09-21, by wenzelm
added is_ml_reserved;
2006-09-21, by wenzelm
member (op =);
2006-09-21, by wenzelm
serial numbers for types;
2006-09-21, by wenzelm
added dest_binop;
2006-09-21, by wenzelm
member (op =);
2006-09-21, by wenzelm
member (op =);
2006-09-21, by wenzelm
tuned eta_contract;
2006-09-21, by wenzelm
added dest_equals_rhs;
2006-09-21, by wenzelm
tuned;
2006-09-21, by wenzelm
serial numbers for consts;
2006-09-21, by wenzelm
Thm.dest_binop;
2006-09-21, by wenzelm
member (op =);
2006-09-21, by wenzelm
member (op =);
2006-09-21, by wenzelm
updated timings;
2006-09-21, by wenzelm
new function hashw_int
2006-09-21, by paulson
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
2006-09-21, by paulson
corrected for the translation from _ to __ in c_COMBx_e
2006-09-21, by paulson
changed constants into abbreviations; shortened proofs
2006-09-21, by huffman
XML syntax for types, terms, and proofs.
2006-09-21, by berghofe
Added xml_syntax.ML
2006-09-21, by berghofe
Added Tools/xml_syntax.ML
2006-09-21, by berghofe
circumvented defect in SML/NJ type inference
2006-09-21, by haftmann
1. Function package accepts a parameter (default "some_term"), which specifies the functions
2006-09-21, by krauss
removed division_by_zero class requirements from several lemmas
2006-09-21, by huffman
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
2006-09-21, by huffman
choose gnuplot terminal by platform
2006-09-20, by isatest
set terminal png color -- works for older versions of gnuplot;
2006-09-20, by wenzelm
added ZF-UNITY;
2006-09-20, by wenzelm
tidied
2006-09-20, by paulson
Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.
2006-09-20, by mengj
make it work on sunbroy2
2006-09-20, by isatest
Moved the functional equality axioms to helper1 files.
2006-09-20, by mengj
Introduced combinators B', C' and S'.
2006-09-20, by mengj
Removed include_min_comb and include_combS.
2006-09-20, by mengj
Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.
2006-09-20, by aspinall
improvements for codegen 2
2006-09-20, by haftmann
name shifts
2006-09-20, by haftmann
fixed bug
2006-09-20, by haftmann
Removed "induct set" attribute from total induction rules
2006-09-20, by krauss
removed debug
2006-09-20, by haftmann
Fixed error in pattern splitting algorithm
2006-09-20, by krauss
change section to subsection
2006-09-20, by huffman
add header
2006-09-20, by huffman
renamed axclass_xxxx axclasses;
2006-09-20, by wenzelm
tuned;
2006-09-19, by wenzelm
added standard;
2006-09-19, by wenzelm
added name_classrel/arities/arity;
2006-09-19, by wenzelm
pretty_full_theory: suppress internal entities by default;
2006-09-19, by wenzelm
Logic.name_classrel/arities;
2006-09-19, by wenzelm
revert to previous version;
2006-09-19, by wenzelm
added General/susp.ML;
2006-09-19, by wenzelm
removed duplicate arities;
2006-09-19, by wenzelm
sko/abs: Name.internal prevents choking of print_theory;
2006-09-19, by wenzelm
tuned method setup;
2006-09-19, by wenzelm
tuned proofs;
2006-09-19, by wenzelm
'print_theory': bang option for full verbosity;
2006-09-19, by wenzelm
* Pure: 'print_theory' now suppresses entities with internal name;
2006-09-19, by wenzelm
tuned;
2006-09-19, by wenzelm
simple html output;
2006-09-19, by wenzelm
timespan: 100 days;
2006-09-19, by wenzelm
superceded by isatest-statistics;
2006-09-19, by wenzelm
tuned;
2006-09-19, by wenzelm
target dir;
2006-09-19, by wenzelm
Standard statistics.
2006-09-19, by wenzelm
time: include year;
2006-09-19, by wenzelm
Produce statistics from isatest session logs.
2006-09-19, by wenzelm
moved Import/susp.ML to Pure/General;
2006-09-19, by wenzelm
renamed axclass_xxxx axclasses
2006-09-19, by obua
removed diagnostic messages
2006-09-19, by haftmann
Operational Equality
2006-09-19, by haftmann
this file contains a compile-challenge suggested by Adam Chlipala;
2006-09-19, by urbanc
tuned
2006-09-19, by urbanc
added auxiliary lemma for code generation 2
2006-09-19, by haftmann
removed
2006-09-19, by haftmann
moved part of normalization oracle here
2006-09-19, by haftmann
classical arity syntax
2006-09-19, by haftmann
added codegen_data
2006-09-19, by haftmann
moved base setup for evaluation oracle hier
2006-09-19, by haftmann
added OperationalEquality.thy
2006-09-19, by haftmann
code generation 2 adjustments
2006-09-19, by haftmann
(void)
2006-09-19, by haftmann
improved numeral handling for nbe
2006-09-19, by haftmann
added suspensions in Pure
2006-09-19, by haftmann
added some stuff for code generation 2
2006-09-19, by haftmann
dropped error-prone code generation 2 for wfrec
2006-09-19, by haftmann
text cleanup
2006-09-19, by haftmann
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
2006-09-19, by haftmann
explicit divmod algorithm for code generation
2006-09-19, by haftmann
added operational equality
2006-09-19, by haftmann
added section on code generation 2
2006-09-19, by haftmann
code_gen now peek keyword
2006-09-19, by haftmann
cleanupdiff
2006-09-19, by haftmann
added classes real_div_algebra and real_field; added lemmas
2006-09-19, by huffman
add Real/RealVector.thy
2006-09-19, by huffman
* Pure: 'class_deps' command visualizes the subclass relation;
2006-09-18, by wenzelm
added class_deps;
2006-09-18, by wenzelm
added dest_arg, i.e. a tuned version of #2 o dest_comb;
2006-09-18, by wenzelm
Thm.dest_arg;
2006-09-18, by wenzelm
Present.display_graph;
2006-09-18, by wenzelm
added display_graph (from thm_deps.ML);
2006-09-18, by wenzelm
output: uninterpreted raw symbols -- these are usually LaTeX macros;
2006-09-18, by wenzelm
pretty_thm: graceful treatment of ProtoPure.thy;
2006-09-18, by wenzelm
added class_deps;
2006-09-18, by wenzelm
classes: maintain serial number;
2006-09-18, by wenzelm
tuned;
2006-09-18, by wenzelm
isatool browser: renamed option -d to -c (cf. isatool tool)
2006-09-18, by wenzelm
PRIVATE_FILE: slightly more robust way to create and dispose;
2006-09-18, by wenzelm
renamed option -d to -c (cf. isatool display);
2006-09-18, by wenzelm
updated;
2006-09-18, by wenzelm
Bug fix to prevent exception dest_Free from escaping
2006-09-18, by paulson
Added the max_new parameter, which is a cap on how many clauses may be admitted per round.
2006-09-18, by paulson
replaced implodeable_Ext by set_like
2006-09-18, by obua
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
2006-09-18, by chaieb
replace (x + - y) with (x - y)
2006-09-18, by huffman
add type constraint to otherwise looping iff rule
2006-09-17, by huffman
generalize type of (NS)LIM to work on functions with vector space domain types
2006-09-17, by huffman
norm_one is now proved from other class axioms
2006-09-17, by huffman
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
2006-09-17, by huffman
hcmod abbreviates hnorm :: hcomplex => hypreal
2006-09-17, by huffman
complex_of_real abbreviates of_real::real=>complex;
2006-09-16, by huffman
add instance for real_algebra_1 and real_normed_div_algebra
2006-09-16, by huffman
add instances for real_vector and real_algebra
2006-09-16, by huffman
define new constant of_real for class real_algebra_1;
2006-09-16, by huffman
int_diff_cases moved to Integ/IntDef.thy
2006-09-16, by huffman
generalized types of many constants to work over arbitrary vector spaces;
2006-09-16, by huffman
add theorem norm_diff_triangle_ineq
2006-09-16, by huffman
add required type annotation
2006-09-16, by huffman
removed type aliases for theory/theory_ref;
2006-09-15, by wenzelm
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-15, by wenzelm
tuned;
2006-09-15, by wenzelm
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
2006-09-15, by wenzelm
instantiate: omit has_duplicates check, which is irrelevant for soundness;
2006-09-15, by wenzelm
trivial whitespace change
2006-09-15, by webertj
tuned;
2006-09-15, by wenzelm
more on theorems;
2006-09-14, by wenzelm
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
2006-09-14, by huffman
add instance for class division_ring
2006-09-14, by huffman
removed duplicate lemmas
2006-09-14, by huffman
fixed syntax clash with Real/RealVector
2006-09-14, by huffman
*** empty log message ***
2006-09-14, by wenzelm
Function package: Outside their domain functions now return "arbitrary".
2006-09-14, by krauss
updated makefile
2006-09-14, by krauss
Fixed Subscript Exception occurring with Higher-Order recursion
2006-09-14, by krauss
remove conflicting norm syntax
2006-09-14, by huffman
made SML/NJ happy;
2006-09-14, by wenzelm
added exists_type;
2006-09-13, by wenzelm
renamed NameSpace.drop_base to NameSpace.qualifier;
2006-09-13, by wenzelm
Updated keyword file
2006-09-13, by krauss
Removed debugging code imports...
2006-09-13, by krauss
Added the "theory_const" option. Only it is OFF because it's often harmful!
2006-09-13, by paulson
Extended the blacklist with higher-order theorems. Restructured. Added checks to
2006-09-13, by paulson
bug fix to abstractions: free variables in theorem can be abstracted over.
2006-09-13, by paulson
Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective
2006-09-13, by paulson
Major update to function package, including new syntax and the (only theoretical)
2006-09-13, by krauss
added instance rat :: recpower
2006-09-13, by huffman
more on theorems;
2006-09-12, by wenzelm
tuned;
2006-09-12, by wenzelm
more on terms;
2006-09-12, by wenzelm
no_syntax norm -- clash with Real/RealVector.thy;
2006-09-12, by wenzelm
simplify some proofs, remove obsolete realpow_divide
2006-09-12, by huffman
realpow_divide -> power_divide
2006-09-12, by huffman
remove extra dependency
2006-09-12, by huffman
more on terms;
2006-09-12, by wenzelm
Efficient term substitution -- avoids copying.
2006-09-12, by wenzelm
ctyp: maintain maxidx;
2006-09-12, by wenzelm
removed obsolete aconvs (use eq_list aconv);
2006-09-12, by wenzelm
tuned eq_list;
2006-09-12, by wenzelm
moved term subst functions to TermSubst;
2006-09-12, by wenzelm
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
2006-09-12, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip