| author | blanchet | 
| Tue, 02 Sep 2014 12:13:32 +0200 | |
| changeset 58138 | 3bfd12e456f4 | 
| parent 35762 | af3ff2ba4c54 | 
| permissions | -rw-r--r-- | 
| 
26056
 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
 
krauss 
parents: 
24893 
diff
changeset
 | 
1  | 
theory Main  | 
| 
 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
 
krauss 
parents: 
24893 
diff
changeset
 | 
2  | 
imports Main_ZF  | 
| 
 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
 
krauss 
parents: 
24893 
diff
changeset
 | 
3  | 
begin  | 
| 12620 | 4  | 
|
| 12426 | 5  | 
end  |