Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. added lambda-free HO output for Ehoh (higher-order E prototype)
  2. First step to remove nonstandard "[x <- xs. P]" syntax: only input
  3. merged
  4. removed unicode symbol
  5. Moved Landau_Symbols from the AFP to HOL-Library
  6. merged
  7. more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
Changeset 68250:c45067867860 by blanchet:
added lambda-free HO output for Ehoh (higher-order E prototype)
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/ATP/atp_problem.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 68249:949d93804740 by nipkow:
First step to remove nonstandard &quot;[x &lt;- xs. P]&quot; syntax: only input
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Inner_Syntax.thy (diff)
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/Doc/Tutorial/Inductive/AB.thy (diff)
The file was modified src/HOL/Library/AList.thy (diff)
The file was modified src/HOL/Library/Finite_Map.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/MicroJava/DFA/Kildall.thy (diff)
The file was modified src/HOL/MicroJava/DFA/LBVComplete.thy (diff)
The file was modified src/HOL/MicroJava/DFA/LBVCorrect.thy (diff)
The file was modified src/HOL/MicroJava/DFA/LBVSpec.thy (diff)
The file was modified src/HOL/MicroJava/DFA/SemilatAlg.thy (diff)
The file was modified src/HOL/Nitpick_Examples/Manual_Nits.thy (diff)
The file was modified src/HOL/Nominal/Examples/W.thy (diff)
The file was modified src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy (diff)
The file was modified src/HOL/Probability/Probability_Mass_Function.thy (diff)
The file was modified src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy (diff)
The file was modified src/HOL/Quotient_Examples/Quotient_FSet.thy (diff)
The file was modified src/HOL/Random.thy (diff)
The file was modified src/HOL/ex/Quicksort.thy (diff)
The file was modified src/HOL/ex/Radix_Sort.thy (diff)
Changeset 68248:ef1e0cb80fde by nipkow:
merged
Changeset 68247:7344affc0bd4 by nipkow:
removed unicode symbol
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
Changeset 68246:b48bab511939 by manuel eberl _eberlm@in.tum.de_:
Moved Landau_Symbols from the AFP to HOL-Library
The file was addedsrc/HOL/Library/Landau_Symbols.thy
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Library.thy (diff)
Changeset 68245:37974ddde928 by wenzelm:
merged
Changeset 68244:e0cd57aeb60c by wenzelm:
more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
The file was modified src/Pure/global_theory.ML (diff)