src/HOL/Proofs.thy
author traytel
Fri, 02 Aug 2013 12:08:55 +0200
changeset 52839 2c0e1a84dcc7
parent 52488 cd65ee49a8ba
permissions -rw-r--r--
store relator induction in fp_result

theory Proofs
imports Pure
begin

ML "Proofterm.proofs := 2"

end