| 2018-01-10 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| 2017-11-26 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2017-08-07 |
blanchet |
tuning imports
|
file |
diff |
annotate
|
| 2016-12-22 |
haftmann |
proper logical constants
|
file |
diff |
annotate
|
| 2016-07-29 |
Andreas Lochbihler |
add lemmas contributed by Peter Gammie
|
file |
diff |
annotate
|
| 2016-02-23 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| 2015-12-13 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| 2015-11-09 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| 2015-11-04 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2015-04-14 |
Andreas Lochbihler |
move lemma from AFP/Coinductive
|
file |
diff |
annotate
|
| 2015-03-07 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
file |
diff |
annotate
|
| 2015-02-11 |
Andreas Lochbihler |
add lemmas about flat_ord
|
file |
diff |
annotate
|
| 2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| 2014-08-16 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| 2014-01-20 |
blanchet |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
|
file |
diff |
annotate
|
| 2013-12-05 |
Andreas Lochbihler |
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
|
file |
diff |
annotate
|
| 2013-09-27 |
Andreas Lochbihler |
generalise lemma
|
file |
diff |
annotate
|
| 2013-09-02 |
Andreas Lochbihler |
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
|
file |
diff |
annotate
|
| 2013-07-24 |
krauss |
derive specialized version of full fixpoint induction (with admissibility)
|
file |
diff |
annotate
|
| 2013-03-21 |
krauss |
added rudimentary induction rule for partial_function (heap)
|
file |
diff |
annotate
|
| 2013-03-19 |
Andreas Lochbihler |
add induction rule for partial_function (tailrec)
|
file |
diff |
annotate
|
| 2012-08-22 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| 2012-03-15 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| 2011-12-29 |
huffman |
remove constant 'ccpo.lub', re-use constant 'Sup' instead
|
file |
diff |
annotate
|
| 2011-10-29 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2011-05-31 |
krauss |
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
|
file |
diff |
annotate
|
| 2011-05-31 |
krauss |
admissibility on option type
|
file |
diff |
annotate
|
| 2011-05-23 |
krauss |
also manage induction rule;
|
file |
diff |
annotate
|
| 2011-05-23 |
krauss |
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
|
file |
diff |
annotate
|