changeset 35954 | d87d85a5d9ab |
parent 35950 | 791ce568d40a |
child 36040 | fcd7bea01a93 |
35953:0460ff79bb52 | 35954:d87d85a5d9ab |
---|---|
1 theory Predicate_Compile_Examples |
1 theory Predicate_Compile_Examples |
2 imports "../ex/Predicate_Compile_Alternative_Defs" |
2 imports Predicate_Compile_Alternative_Defs |
3 begin |
3 begin |
4 |
4 |
5 subsection {* Basic predicates *} |
5 subsection {* Basic predicates *} |
6 |
6 |
7 inductive False' :: "bool" |
7 inductive False' :: "bool" |