| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
daac7840 |
|
07-Aug-2017 |
blanchet <none@none> |
tuning imports
|
| #
241de186 |
|
22-Dec-2016 |
haftmann <none@none> |
proper logical constants
|
| #
65b76842 |
|
29-Jul-2016 |
Andreas Lochbihler <none@none> |
add lemmas contributed by Peter Gammie
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;
|
| #
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
| #
8e8b881c |
|
04-Nov-2015 |
ballarin <none@none> |
Keyword 'rewrites' identifies rewrite morphisms.
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
b7949a9e |
|
14-Apr-2015 |
Andreas Lochbihler <none@none> |
move lemma from AFP/Coinductive
|
| #
c97e9ad6 |
|
07-Mar-2015 |
wenzelm <none@none> |
clarified Drule.gen_all: observe context more carefully;
|
| #
5c49d04b |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
add lemmas about flat_ord
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
9067b570 |
|
16-Aug-2014 |
wenzelm <none@none> |
updated to named_theorems;
modernized module name and setup;
|
| #
d46ef5de |
|
20-Jan-2014 |
blanchet <none@none> |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
--HG--
rename : src/HOL/FunDef.thy => src/HOL/Fun_Def.thy
|
| #
eb5ad205 |
|
05-Dec-2013 |
Andreas Lochbihler <none@none> |
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
|
| #
dbc0b003 |
|
26-Sep-2013 |
Andreas Lochbihler <none@none> |
generalise lemma
|
| #
a69c3d9e |
|
02-Sep-2013 |
Andreas Lochbihler <none@none> |
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
|
| #
3cde49ef |
|
24-Jul-2013 |
krauss <none@none> |
derive specialized version of full fixpoint induction (with admissibility)
|
| #
2d78fd74 |
|
21-Mar-2013 |
krauss <none@none> |
added rudimentary induction rule for partial_function (heap)
|
| #
2953cc4e |
|
19-Mar-2013 |
Andreas Lochbihler <none@none> |
add induction rule for partial_function (tailrec)
|
| #
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
| #
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
| #
d7898d1c |
|
29-Dec-2011 |
huffman <none@none> |
remove constant 'ccpo.lub', re-use constant 'Sup' instead
|
| #
de8d7d09 |
|
28-Oct-2011 |
wenzelm <none@none> |
tuned;
|
| #
99efaaae |
|
31-May-2011 |
krauss <none@none> |
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
|
| #
b51fdce3 |
|
31-May-2011 |
krauss <none@none> |
admissibility on option type
|
| #
e73bb49a |
|
23-May-2011 |
krauss <none@none> |
also manage induction rule;
tuned data slot
|
| #
bc71ee3c |
|
23-May-2011 |
krauss <none@none> |
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
|
| #
6ad35720 |
|
29-Oct-2010 |
krauss <none@none> |
added rule let_mono
|
| #
fe7556fe |
|
29-Oct-2010 |
krauss <none@none> |
hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
|
| #
ae451101 |
|
23-Oct-2010 |
krauss <none@none> |
first version of partial_function package
|