# HG changeset patch # User aspinall # Date 1092671767 -7200 # Node ID 87c074aad0073bcf7ac5f7f39efb9bde16a5bd1e # Parent df2b7976d1e79626677b0109dc488c7bd484634c Experimental pgip_isar.xml file diff -r df2b7976d1e7 -r 87c074aad007 lib/ProofGeneral/pgip_isar.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/ProofGeneral/pgip_isar.xml Mon Aug 16 17:56:07 2004 +0200 @@ -0,0 +1,147 @@ + + + + + + + + + + + + + + + + theorem + lemma + corollary + + + + + + + + + + + + + + + + + + + R0lGODlhJgAgAIQAAP////r6+uDg4Nra2tnZ2fn5+WFhYUJCQkFBQWBgYMnO + 91xq6K208wsg3XiD7OTm+0FR5CY54Pb29t3d3dfX119fX/T09NbW1tjY2AAA + AAAAAAAAAAAAAAAAAAAAAAAAACH+FUNyZWF0ZWQgd2l0aCBUaGUgR0lNUAAh + +QQBCgAfACwAAAAAJgAgAAAFnCAgjmRpnqgYCAPhvnAsz7BQAIJxIHzv/8Cg + LyHA6YTI5I8IWLVo0Gjtlqpar9istqRYLBTbMIDRaDDEW7IZrVWf2VYGw1F2 + yBkP+KnM77/1Jm6AcWV/gyeChyiJioGFjYiPkCWMkyKVlpiTmpBqEJYlEWUR + XgugDBCjDnmgrZMSExQUUrQ0NgADFUq7SUy5vMBATBYDFxi1yFMAIQA7 + + + + + R0lGODlhJgAgAIQAAP////r6+uDg4Nra2tnZ2fn5+WFhYUJCQkFBQWBgYOTm + +62080FR5Asg3SY54Fxq6MnO95Kc73iD7Pb29t3d3dfX119fX/T09NbW1tjY + 2AAAAAAAAAAAAAAAAAAAAAAAACH+FUNyZWF0ZWQgd2l0aCBUaGUgR0lNUAAh + +QQBCgAfACwAAAAAJgAgAAAFsyAgjmRpnqgYCAPhvnAsz7BQAIJxIHzv/8Cg + LyHA6YTI5I8IWLVo0Gjtlqpar9istqRYeL9exbaqYDTOaPRijFI40vDGmm16 + NB74NwOPh9C5DWIidn9VERIkb4UpEYIiZ4tZkJFWEA0MlFYLd5lVmw+dKZ8k + fqEim4GnoKYAlndiDIisAG9ppawSaauzALkNsrzBwsPEIxMUFRVSyzQ2AAMW + StJJTNDT10BMFwMYGczfUwAhADs= + + + + + + + + + + + theorem + + declare %1 [simp] + + + + theorem + + declare %1 [simp del] + + + + theorem term + theorem + %1 [OF %2] + + + + + + + Input a term: + + + term + term %term + + + + + ruleset + apply (rule %1) + + + ruleset + apply (erule %1) + + + ruleset + apply (drule %1) + + + + + + + Input a name: + Input a term: + + + + [simp] + + Attributes: + + + lemma %attributes %name : "%term" + + + +