| #
56af848c |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
04a2ad4d |
|
02-Jan-2018 |
blanchet <none@none> |
updated dependencies + compile
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
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;
|
| #
99807201 |
|
17-Feb-2014 |
blanchet <none@none> |
name derivations in 'primrec' for code extraction from proof terms
|
| #
3e0fffd8 |
|
24-Feb-2013 |
wenzelm <none@none> |
prefer stateless 'ML_val' for tests;
|
| #
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
|
| #
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
|
| #
3d40d3d4 |
|
29-Dec-2010 |
wenzelm <none@none> |
explicit file specifications -- avoid secondary load path;
|
| #
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
|