Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. more explicit dummy proofs;
  2. more explicit dummy proofs;
  3. unused;
  4. command '\<proof>' is an alias for 'sorry', with different typesetting;
  5. more antiquotations;
  6. more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
Changeset 62315:ccb42dbf4aa1 by wenzelm:
more explicit dummy proofs;
The file was modified src/HOL/Induct/Common_Patterns.thy (diff)
Changeset 62314:ec0fbd1a852b by wenzelm:
more explicit dummy proofs;
The file was modified src/HOL/Isar_Examples/Structured_Statements.thy (diff)
The file was modified src/HOL/Isar_Examples/document/root.tex (diff)
Changeset 62313:aaeee16a56f5 by wenzelm:
unused;
The file was modified src/HOL/Imperative_HOL/document/root.tex (diff)
Changeset 62312:5e5a881ebc12 by wenzelm:
command &#039;\&lt;proof&gt;&#039; is an alias for &#039;sorry&#039;, with different typesetting;
The file was modified NEWS (diff)
The file was modified lib/texinputs/isabellesym.sty (diff)
The file was modified src/Doc/Isar_Ref/Base.thy (diff)
The file was modified src/Doc/Isar_Ref/document/style.sty (diff)
The file was modified src/HOL/Imperative_HOL/document/root.tex (diff)
The file was modified src/Pure/Isar/isar_syn.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 62311:73bebf642d3b by wenzelm:
more antiquotations;
The file was modified src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy (diff)
Changeset 62310:ab836dc7410e by wenzelm:
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
The file was modified src/Pure/PIDE/prover.scala (diff)