#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
844a31ab |
|
30-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
962c2adf |
|
18-Sep-2014 |
blanchet <none@none> |
tuned imports
|
#
392cced7 |
|
18-Sep-2014 |
blanchet <none@none> |
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again --HG-- rename : src/HOL/Old_Datatype.thy => src/HOL/Library/Old_Datatype.thy
|
#
ade011bf |
|
10-Nov-2013 |
haftmann <none@none> |
qualifed popular user space names
|
#
ab81b51e |
|
17-Feb-2012 |
wenzelm <none@none> |
simplified configuration options for syntax ambiguity;
|
#
c94a7d0e |
|
16-Feb-2012 |
wenzelm <none@none> |
simplified configuration options for syntax ambiguity;
|
#
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
#
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
|