Diffusion Isabelle b49bd5d9041f

improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
b49bd5d9041f
Actions

Description

improper proof command 'guess' moved to separate theory "Pure-ex.Guess";

Details

Provenance

makarius

Authored on

Parents

rISABELLE383fd113baae: merged

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLEb49bd5d9041f: improper proof command 'guess' moved to separate theory "Pure-ex.Guess";.Sep 26 2021, 6:49 PM

makarius mentioned this in rAFP2056abab0dd6: mproper proof command 'guess' moved to separate theory "Pure-ex.Guess"….Sep 26 2021, 8:50 PM

makarius mentioned this in Blog Post: Improper proof command 'guess' provided by separate theory "Pure-ex.Guess".Sep 27 2021, 5:00 PM

Changes (15)

Path

Size

NEWS

src

Doc/

Implementation/

Isar_Ref/

Isar/

	Pure/	ex/
	HOL/	ex/

	Guess_Examples.thy
	Guess.thy

rISABELLEb49bd5d9041f

View Options

NEWS

View Options

src/Doc/Implementation/Proof.thy

View Options

src/Doc/Isar_Ref/Proof.thy

View Options

src/HOL/ROOT

View Options

src/HOL/ex/Guess.thy

View Options

src/Pure/Isar/obtain.ML

View Options

src/Pure/Pure.thy

View Options

src/Pure/ROOT

View Options

src/Pure/ex/Guess.thy

View Options

src/Pure/ex/Guess_Examples.thy

improper proof command 'guess' moved to separate theory "Pure-ex.Guess";b49bd5d9041fActions

Description

Details

Event Timeline

Changes (15)

rISABELLEb49bd5d9041f

NEWS

src/Doc/Implementation/Proof.thy

src/Doc/Isar_Ref/Proof.thy

src/HOL/ROOT

src/HOL/ex/Guess.thy

src/Pure/Isar/obtain.ML

src/Pure/Pure.thy

src/Pure/ROOT

src/Pure/ex/Guess.thy

src/Pure/ex/Guess_Examples.thy

improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
b49bd5d9041f
Actions