equal
deleted
inserted
replaced
14 type format = ATP_Problem.format |
14 type format = ATP_Problem.format |
15 type formula_kind = ATP_Problem.formula_kind |
15 type formula_kind = ATP_Problem.formula_kind |
16 type 'a problem = 'a ATP_Problem.problem |
16 type 'a problem = 'a ATP_Problem.problem |
17 |
17 |
18 datatype locality = |
18 datatype locality = |
19 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | |
19 General | Helper | Induction | Extensionality | Intro | Elim | Simp | |
20 Chained |
20 Local | Assum | Chained |
21 |
21 |
22 datatype order = First_Order | Higher_Order |
22 datatype order = First_Order | Higher_Order |
23 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic |
23 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic |
24 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound |
24 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound |
25 datatype type_level = |
25 datatype type_level = |
525 val name = `make_bound_var s |
525 val name = `make_bound_var s |
526 val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t |
526 val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t |
527 in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end |
527 in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end |
528 |
528 |
529 datatype locality = |
529 datatype locality = |
530 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | |
530 General | Helper | Induction | Extensionality | Intro | Elim | Simp | |
531 Chained |
531 Local | Assum | Chained |
532 |
532 |
533 datatype order = First_Order | Higher_Order |
533 datatype order = First_Order | Higher_Order |
534 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic |
534 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic |
535 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound |
535 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound |
536 datatype type_level = |
536 datatype type_level = |