| #
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
|