| author | huffman | 
| Wed, 03 Mar 2010 20:20:41 -0800 | |
| changeset 35564 | 20995afa8fa1 | 
| parent 34205 | f69cd974bc4e | 
| child 37296 | 1fad5b94c0ae | 
| permissions | -rw-r--r-- | 
| 11943 | 1 | Syntax.ambiguity_level := 100; | 
| 25374 | 2 | Proofterm.proofs := 2; | 
| 11943 | 3 | |
| 26748 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
 krauss parents: 
25374diff
changeset | 4 | no_document use_thys ["Code_Integer"]; | 
| 34205 
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
 wenzelm parents: 
33615diff
changeset | 5 | use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"]; |