equal
deleted
inserted
replaced
1078 |
1078 |
1079 (** axioms and theorems **) |
1079 (** axioms and theorems **) |
1080 |
1080 |
1081 fun vars_of t = map Var (rev (Term.add_vars t [])); |
1081 fun vars_of t = map Var (rev (Term.add_vars t [])); |
1082 fun frees_of t = map Free (rev (Term.add_frees t [])); |
1082 fun frees_of t = map Free (rev (Term.add_frees t [])); |
|
1083 fun variables_of t = vars_of t @ frees_of t; |
1083 |
1084 |
1084 fun test_args _ [] = true |
1085 fun test_args _ [] = true |
1085 | test_args is (Bound i :: ts) = |
1086 | test_args is (Bound i :: ts) = |
1086 not (member (op =) is i) andalso test_args (i :: is) ts |
1087 not (member (op =) is i) andalso test_args (i :: is) ts |
1087 | test_args _ _ = false; |
1088 | test_args _ _ = false; |
1564 (** reconstruction of partial proof terms **) |
1565 (** reconstruction of partial proof terms **) |
1565 |
1566 |
1566 local |
1567 local |
1567 |
1568 |
1568 exception MIN_PROOF of unit; |
1569 exception MIN_PROOF of unit; |
1569 |
|
1570 fun vars_of t = map Var (rev (Term.add_vars t [])); |
|
1571 fun frees_of t = map Free (rev (Term.add_frees t [])); |
|
1572 fun variables_of t = vars_of t @ frees_of t; |
|
1573 |
1570 |
1574 fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop; |
1571 fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop; |
1575 fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf; |
1572 fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf; |
1576 |
1573 |
1577 fun app_types shift prop Ts prf = |
1574 fun app_types shift prop Ts prf = |