#
04a2ad4d |
|
02-Jan-2018 |
blanchet <none@none> |
updated dependencies + compile
|
#
572e4d03 |
|
21-Apr-2017 |
wenzelm <none@none> |
clarified imports;
|
#
5cca9e8d |
|
26-Apr-2016 |
wenzelm <none@none> |
some uses of 'obtain' with structure statement;
|
#
844a31ab |
|
30-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
03e209c5 |
|
21-Apr-2015 |
nipkow <none@none> |
added simp rules for ==>
|
#
222bbb17 |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
5f318eee |
|
04-Mar-2015 |
wenzelm <none@none> |
clarified signature;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
f2f7425c |
|
07-Oct-2014 |
wenzelm <none@none> |
more antiquotations;
|
#
962c2adf |
|
18-Sep-2014 |
blanchet <none@none> |
tuned imports
|
#
713cd402 |
|
13-Mar-2014 |
nipkow <none@none> |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions --HG-- extra : rebase_source : 4103bf02b2df95e1e84808f766f131292beef893
|
#
5a8927d0 |
|
15-Feb-2013 |
haftmann <none@none> |
two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one --HG-- extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17
|
#
b11913f5 |
|
03-Dec-2012 |
blanchet <none@none> |
renamed "Type.thy" to something that's less likely to cause conflicts --HG-- rename : src/HOL/Proofs/Lambda/Type.thy => src/HOL/Proofs/Lambda/LambdaType.thy
|
#
844a16cc |
|
27-Nov-2012 |
wenzelm <none@none> |
eliminated some improper identifiers;
|
#
a6699ffc |
|
19-Oct-2011 |
bulwahn <none@none> |
removing invocations of the old code generator
|
#
4d9b7a48 |
|
26-Jul-2011 |
bulwahn <none@none> |
adding remarks after static inspection of the invocation of the SML code generator
|
#
d1a2ff7b |
|
16-Apr-2011 |
wenzelm <none@none> |
eliminated old List.nth; tuned;
|
#
3d40d3d4 |
|
29-Dec-2010 |
wenzelm <none@none> |
explicit file specifications -- avoid secondary load path;
|
#
14e6bac1 |
|
19-Nov-2010 |
wenzelm <none@none> |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
#
6fc20f26 |
|
06-Sep-2010 |
wenzelm <none@none> |
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); --HG-- rename : src/HOL/Extraction/Euclid.thy => src/HOL/Proofs/Extraction/Euclid.thy rename : src/HOL/Extraction/Greatest_Common_Divisor.thy => src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy rename : src/HOL/Extraction/Higman.thy => src/HOL/Proofs/Extraction/Higman.thy rename : src/HOL/Extraction/Pigeonhole.thy => src/HOL/Proofs/Extraction/Pigeonhole.thy rename : src/HOL/Extraction/QuotRem.thy => src/HOL/Proofs/Extraction/QuotRem.thy rename : src/HOL/Extraction/ROOT.ML => src/HOL/Proofs/Extraction/ROOT.ML rename : src/HOL/Extraction/Util.thy => src/HOL/Proofs/Extraction/Util.thy rename : src/HOL/Extraction/Warshall.thy => src/HOL/Proofs/Extraction/Warshall.thy rename : src/HOL/Extraction/document/root.bib => src/HOL/Proofs/Extraction/document/root.bib rename : src/HOL/Extraction/document/root.tex => src/HOL/Proofs/Extraction/document/root.tex rename : src/HOL/Lambda/Commutation.thy => src/HOL/Proofs/Lambda/Commutation.thy rename : src/HOL/Lambda/Eta.thy => src/HOL/Proofs/Lambda/Eta.thy rename : src/HOL/Lambda/InductTermi.thy => src/HOL/Proofs/Lambda/InductTermi.thy rename : src/HOL/Lambda/Lambda.thy => src/HOL/Proofs/Lambda/Lambda.thy rename : src/HOL/Lambda/ListApplication.thy => src/HOL/Proofs/Lambda/ListApplication.thy rename : src/HOL/Lambda/ListBeta.thy => src/HOL/Proofs/Lambda/ListBeta.thy rename : src/HOL/Lambda/ListOrder.thy => src/HOL/Proofs/Lambda/ListOrder.thy rename : src/HOL/Lambda/NormalForm.thy => src/HOL/Proofs/Lambda/NormalForm.thy rename : src/HOL/Lambda/ParRed.thy => src/HOL/Proofs/Lambda/ParRed.thy rename : src/HOL/Lambda/README.html => src/HOL/Proofs/Lambda/README.html rename : src/HOL/Lambda/ROOT.ML => src/HOL/Proofs/Lambda/ROOT.ML rename : src/HOL/Lambda/Standardization.thy => src/HOL/Proofs/Lambda/Standardization.thy rename : src/HOL/Lambda/StrongNorm.thy => src/HOL/Proofs/Lambda/StrongNorm.thy rename : src/HOL/Lambda/Type.thy => src/HOL/Proofs/Lambda/Type.thy rename : src/HOL/Lambda/WeakNorm.thy => src/HOL/Proofs/Lambda/WeakNorm.thy rename : src/HOL/Lambda/document/root.bib => src/HOL/Proofs/Lambda/document/root.bib rename : src/HOL/Lambda/document/root.tex => src/HOL/Proofs/Lambda/document/root.tex rename : src/HOL/ex/Hilbert_Classical.thy => src/HOL/Proofs/ex/Hilbert_Classical.thy
|