author | blanchet |
Mon, 21 May 2012 10:39:31 +0200 | |
changeset 47944 | e6b51fab96f7 |
parent 35325 | 4123977b469d |
permissions | -rw-r--r-- |
35325
4123977b469d
adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session
bulwahn
parents:
diff
changeset
|
1 |
|
4123977b469d
adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session
bulwahn
parents:
diff
changeset
|
2 |
use_thy "MutabelleExtra"; |
4123977b469d
adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session
bulwahn
parents:
diff
changeset
|
3 |