theory Guess_Examples imports"Pure-Examples.Higher_Order_Logic"Guess begin
typedecl t instance t :: type ..
notepad begin have 1: "\x :: 'a. x = x" by (intro exI refl)
from 1 guess .. from 1 guess x .. from 1 guess x :: 'a .. from 1 guess x :: t ..
have 2: "\(x::'c) (y::'d). x = x \ y = y" by (intro exI conjI refl) from 2 guessapply - apply (erule exE conjE)+ done from 2 guess x apply - apply (erule exE conjE)+ done from 2 guess x y apply - apply (erule exE conjE)+ done from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done from 2 guess x y :: t apply - apply (erule exE conjE)+ done end
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
