equal
deleted
inserted
replaced
17 |
17 |
18 session "HOL-Proofs" = Pure + |
18 session "HOL-Proofs" = Pure + |
19 description {* |
19 description {* |
20 HOL-Main with explicit proof terms. |
20 HOL-Main with explicit proof terms. |
21 *} |
21 *} |
22 options [document = false] |
22 options [document = false, quick_and_dirty = false] |
23 theories Proofs (*sequential change of global flag!*) |
23 theories Proofs (*sequential change of global flag!*) |
24 theories "~~/src/HOL/Library/Old_Datatype" |
24 theories "~~/src/HOL/Library/Old_Datatype" |
25 files |
25 files |
26 "Tools/Quickcheck/Narrowing_Engine.hs" |
26 "Tools/Quickcheck/Narrowing_Engine.hs" |
27 "Tools/Quickcheck/PNF_Narrowing_Engine.hs" |
27 "Tools/Quickcheck/PNF_Narrowing_Engine.hs" |
398 |
398 |
399 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + |
399 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + |
400 description {* |
400 description {* |
401 Examples for program extraction in Higher-Order Logic. |
401 Examples for program extraction in Higher-Order Logic. |
402 *} |
402 *} |
403 options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0] |
403 options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false] |
404 theories [document = false] |
404 theories [document = false] |
405 "~~/src/HOL/Library/Code_Target_Numeral" |
405 "~~/src/HOL/Library/Code_Target_Numeral" |
406 "~~/src/HOL/Library/Monad_Syntax" |
406 "~~/src/HOL/Library/Monad_Syntax" |
407 "~~/src/HOL/Number_Theory/Primes" |
407 "~~/src/HOL/Number_Theory/Primes" |
408 "~~/src/HOL/Number_Theory/UniqueFactorization" |
408 "~~/src/HOL/Number_Theory/UniqueFactorization" |
423 proves confluence of beta, eta and beta+eta. |
423 proves confluence of beta, eta and beta+eta. |
424 |
424 |
425 The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole |
425 The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole |
426 theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). |
426 theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). |
427 *} |
427 *} |
428 options [document_graph, print_mode = "no_brackets", parallel_proofs = 0] |
428 options [document_graph, print_mode = "no_brackets", parallel_proofs = 0, |
|
429 quick_and_dirty = false] |
429 theories [document = false] |
430 theories [document = false] |
430 "~~/src/HOL/Library/Code_Target_Int" |
431 "~~/src/HOL/Library/Code_Target_Int" |
431 theories |
432 theories |
432 Eta |
433 Eta |
433 StrongNorm |
434 StrongNorm |