#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
844a31ab |
|
30-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
f2f7425c |
|
07-Oct-2014 |
wenzelm <none@none> |
more antiquotations;
|
#
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;
|
#
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
#
a9cb65ea |
|
22-Sep-2010 |
nipkow <none@none> |
more lists lemmas
|
#
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
|