| author | huffman |
| Tue, 09 Aug 2011 10:42:07 -0700 | |
| changeset 44126 | ce44e70d0c47 |
| 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 |