History log of /seL4-l4v-master/isabelle/src/HOL/Proofs/Lambda/ParRed.thy
Revision Date Author Comments
# 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;
# 34780509 30-Jun-2014 wenzelm <none@none>

removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;
# 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