| #
9e54d1b8 |
|
08-Jul-2017 |
haftmann <none@none> |
dropped superfluous theory imports
|
| #
8ea9d005 |
|
01-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
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;
|
| #
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
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
ca86fe84 |
|
09-Sep-2014 |
blanchet <none@none> |
removed 'datatype_compat's that are no longer needed
|
| #
80186a50 |
|
09-Sep-2014 |
blanchet <none@none> |
ported HOL-Proofs-Extraction to new datatypes
|
| #
b5381478 |
|
22-Sep-2011 |
berghofe <none@none> |
Moved extraction part of Higman's lemma to separate theory to allow reuse in
theories compiled without support for proof terms.
|
| #
4d9b7a48 |
|
26-Jul-2011 |
bulwahn <none@none> |
adding remarks after static inspection of the invocation of the SML code generator
|
| #
3d40d3d4 |
|
29-Dec-2010 |
wenzelm <none@none> |
explicit file specifications -- avoid secondary load path;
|
| #
2b88a692 |
|
04-Nov-2010 |
haftmann <none@none> |
dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
|
| #
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
|