Lines Matching refs:tag
1365 Per evitare la non validit�, � attaccato un \emph{tag} a ogni teorema che deriva
1366 da un oracolo. Questo tag � propagato attraverso ogni inferenza cui quel
1370 tag componenti del teorema. Un teorema dimostrato senza l'uso di
1371 oracoli avr� un tag vuoto, e pu� essere cos� considerato essere stato dimostrato
1383 che crea direttamente il teorema richiesto e attacca ad esso il tag
1384 dato. Il tag � creato attraverso una chiamata a
1389 Tag.read : string -> tag
1394 esterni, i tag sono usati per implementare alcune utili operazioni di `sistema'
1396 funzione \ml{mk\_thm}. Il tag \verb+MK_THM+ viene attaccato ad ogni
1399 derivate. Un altro tag � usato per implementare il cosiddetto `check
1402 I tag in un teorema possono essere visualizzati impostando \verb+Globals.show_tags+ a
1417 stampata di un teorema: i primi due\footnote{I tag sono usati anche per
1418 tenere traccia dell'uso di assiomi nelle dimostrazioni.} comprendono i tag componenti e il
1419 terzo � la lista standard di assunzioni. Il tag componente di un teorema
1424 Thm.tag : thm -> tag
1432 Tag.pp : ppstream -> tag -> unit.