isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 tip

more on built-in syntax transformations, based on reduced version of old material;
2013-06-18, by wenzelm
misc tuning and clarification;
2013-06-18, by wenzelm
more on concrete syntax of proof terms;
2013-06-17, by wenzelm
more on reconstructing and checking proof terms;
2013-06-17, by wenzelm
more examples on proof terms;
2013-06-17, by wenzelm
obsolete;
2013-06-15, by wenzelm
updated operations on proof terms;
2013-06-15, by wenzelm
more on proof terms;
2013-06-15, by wenzelm
updated documentation of sort hypotheses;
2013-06-13, by wenzelm
Explain to beginners why Complex_Main
2013-06-21, by kleing
more set theory
2013-06-21, by nipkow
Code_Real_Approx_By_Float: remove code equations using Ratreal
2013-06-21, by hoelzl
tuned
2013-06-21, by nipkow
added lemma
2013-06-20, by nipkow
tuned theory name
2013-06-20, by nipkow
tuned
2013-06-20, by nipkow
added lemma
2013-06-19, by noschinl
added coprimality lemma
2013-06-19, by noschinl
tuned
2013-06-19, by nipkow
tuned
2013-06-19, by nipkow
more canonical name (2)
2013-06-19, by nipkow
more canonical name
2013-06-19, by nipkow
added lemma
2013-06-19, by nipkow
adjust layout for book
2013-06-18, by kleing
merged
2013-06-18, by nipkow
Added continuity and determinism proof
2013-06-18, by nipkow
Added parantheses to code_type for heap monad
2013-06-18, by lammich
improved defs and proofs
2013-06-18, by nipkow
use \<^isub> in determ proof for display in book
2013-06-17, by kleing
merged
2013-06-17, by krauss
export dom predicate in the info record
2013-06-16, by krauss
export cases rule in the info record
2013-06-16, by krauss
made proofs more readable
2013-06-17, by nipkow
pragmatic executability for instance real :: open
2013-06-15, by haftmann
lifting for primitive definitions;
2013-06-15, by haftmann
selection operator smallest_prime_beyond
2013-06-15, by haftmann
documentation on code_printing and code_identifier
2013-06-15, by haftmann
more consistent parsing and reading of classes and type constructors
2013-06-15, by haftmann
another example lemma
2013-06-14, by kleing
store more theorems in data structure
2013-06-13, by blanchet
tuning
2013-06-13, by blanchet
simplified proofs
2013-06-13, by nipkow
prefer xsymbol for book
2013-06-12, by kleing
same order of properties as in While rule
2013-06-12, by nipkow
some comments on syntax and automation setup
2013-06-11, by kleing
uncheck terms before annotation to avoid awkward syntax
2013-06-11, by smolkas
tuning
2013-06-11, by blanchet
tuning
2013-06-11, by blanchet
make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
2013-06-11, by smolkas
reflexive nbe equation for equality on String.literal
2013-06-11, by haftmann
tuned whitespace
2013-06-10, by haftmann
dropped relics of ancient binary numeral case study
2013-06-10, by haftmann
merged
2013-06-10, by nipkow
all headings in upper case
2013-06-10, by nipkow
more int/nat transfer rules; examples of new untransferred attribute
2013-06-10, by huffman
more transfer rules for sets
2013-06-10, by huffman
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
2013-06-10, by huffman
use right context when exporting variables (cf. AFP Coinductive_List failures)
2013-06-10, by blanchet
keep track of nested BNFs
2013-06-10, by blanchet
tuning
2013-06-10, by blanchet
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
2013-06-08, by huffman
SPASS has more Uppercase keywords than I was fearing -- better always append _
2013-06-07, by blanchet
merge
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
adapted example (cf. 78a3d5006cf1)
2013-06-07, by blanchet
code simplifications (cf. 78a3d5006cf1)
2013-06-07, by blanchet
killed dead code
2013-06-07, by blanchet
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
2013-06-07, by blanchet
killed dead code
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuned
2013-06-07, by nipkow
tuned variable names
2013-06-07, by nipkow
tuned
2013-06-07, by nipkow
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
[mq]: tuning
2013-06-07, by blanchet
tuning
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
fixed failure in coinduction rule tactic
2013-06-06, by blanchet
too much qualification is like too little
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
merge
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
tuned defs
2013-06-06, by nipkow
avoid duplicate call to "mk_fold_rec_args_types" function
2013-06-06, by blanchet
continuation of f461dca57c66
2013-06-06, by blanchet
renamed ML variables
2013-06-06, by blanchet
tuned record field names to avoid confusion between low-level and high-level constants/theorems
2013-06-06, by blanchet
tuned signature
2013-06-06, by blanchet
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
2013-06-06, by blanchet
tuned ML variable names
2013-06-06, by blanchet
transfer rule for listsum
2013-06-05, by kuncar
more reflexivity rules (for OO)
2013-06-05, by kuncar
tuning
2013-06-05, by blanchet
avoid code duplication
2013-06-05, by blanchet
eliminated dead argument
2013-06-05, by blanchet
one less flaky "fpTs" check (flaky in the presence of duplicates in "fpTs", which we want to have in "primrec")
2013-06-05, by blanchet
tuning
2013-06-05, by blanchet
simpler, more robust iterator goal construction code
2013-06-05, by blanchet
tuning
2013-06-05, by blanchet
reverted 23929f647f79 -- not needed after all
2013-06-05, by blanchet
killed dead code
2013-06-05, by blanchet
tuning
2013-06-05, by blanchet
slightly nicer ML interface
2013-06-05, by blanchet
added convenience function
2013-06-05, by blanchet