Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-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 JavaScript-enabled browsers.
tuned;
2010-03-15, by wenzelm
moved old Sign.intern_term to the place where it is still used;
2010-03-15, by wenzelm
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
2010-03-15, by wenzelm
replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-15, by wenzelm
merged
2010-03-15, by haftmann
corrected disastrous syntax declarations
2010-03-15, by haftmann
added stmaryrd for isasymSqinter
2010-03-15, by haftmann
use headers consistently
2010-03-14, by huffman
no_document for theory Countable
2010-03-14, by huffman
old domain package also defines map functions
2010-03-14, by huffman
separate map-related code into new function define_map_functions
2010-03-14, by huffman
removed Local_Theory.theory_result by using local Typedef.add_typedef
2010-03-14, by Christian Urban
tuned comment;
2010-03-14, by wenzelm
observe standard header format;
2010-03-14, by wenzelm
expose formal text;
2010-03-14, by wenzelm
localized @{class} and @{type};
2010-03-14, by wenzelm
move functions into holcf_library.ML
2010-03-14, by huffman
simplify definition of when combinators
2010-03-14, by huffman
declare case_names for various induction rules
2010-03-13, by huffman
add case name 'adm' for infinite induction rules
2010-03-13, by huffman
renamed some lemmas generated by the domain package
2010-03-13, by huffman
use Simplifier.context to avoid 'no proof context in simpset' errors from fixrec_simp after theory merge
2010-03-13, by huffman
fixpat command prints legacy_feature warning
2010-03-13, by huffman
merged
2010-03-13, by huffman
pass binding as argument to add_domain_constructors; proper binding for case combinator
2010-03-13, by huffman
pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names
2010-03-13, by huffman
pass take_info as argument to Domain_Theorems.theorems
2010-03-13, by huffman
replace some string arguments with bindings
2010-03-13, by huffman
more consistent use of qualified bindings
2010-03-13, by huffman
avoid unnecessary primed variable names
2010-03-13, by huffman
remove redundant lemmas
2010-03-13, by huffman
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
2010-03-13, by huffman
fixrec now generates qualified theorem names
2010-03-13, by huffman
no_document for Infinite_Set in HOLCF
2010-03-13, by huffman
removed unused Args.maxidx_values and Element.generalize_facts;
2010-03-13, by wenzelm
Local_Theory.define handles hidden polymorphism;
2010-03-13, by wenzelm
local theory specifications handle hidden polymorphism implicitly;
2010-03-13, by wenzelm
minor tuning and simplification;
2010-03-13, by wenzelm
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
2010-03-13, by wenzelm
removed old CVS Ids;
2010-03-13, by wenzelm
reverted fe9b43a08187 -- "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;
2010-03-13, by wenzelm
merged
2010-03-13, by wenzelm
merged
2010-03-12, by bulwahn
adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
2010-03-12, by bulwahn
adding Spec_Rules to definitional package inductive and inductive_set
2010-03-12, by bulwahn
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
2010-03-12, by bulwahn
merged
2010-03-12, by nipkow
Reorganized Hoare logic theories; added Hoare_Den
2010-03-12, by nipkow
merged
2010-03-12, by hoelzl
reset smt_certificates
2010-03-09, by himmelma
added lemmas
2010-03-09, by himmelma
merged
2010-03-12, by nipkow
Added Hoare_Op.thy
2010-03-12, by nipkow
Equality of integral and infinite sum.
2010-03-12, by hoelzl
make tests less demanding, to prevent sporadic failures
2010-03-12, by blanchet
more antiquotations;
2010-03-13, by wenzelm
command 'typedef' now works within a local theory context;
2010-03-13, by wenzelm
removed obsolete HOL 'typedecl';
2010-03-13, by wenzelm
adapted to localized typedef: handle single global interpretation only;
2010-03-13, by wenzelm
global typedef;
2010-03-13, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip