equal
deleted
inserted
replaced
1 theory Lift |
1 theory Lift |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" |
3 begin |
3 begin |
4 |
4 |
|
5 ML {* |
|
6 fun define_quotient_type args tac ctxt = |
|
7 let |
|
8 val mthd = Method.SIMPLE_METHOD tac |
|
9 val mthdt = Method.Basic (fn _ => mthd) |
|
10 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
|
11 in |
|
12 bymt (Quotient_Type.quotient_type args ctxt) |
|
13 end |
|
14 *} |
|
15 |
|
16 (* Renames schematic variables in a theorem *) |
5 ML {* |
17 ML {* |
6 fun rename_vars fnctn thm = |
18 fun rename_vars fnctn thm = |
7 let |
19 let |
8 val vars = Term.add_vars (prop_of thm) [] |
20 val vars = Term.add_vars (prop_of thm) [] |
9 val nvars = map (Var o ((apfst o apfst) fnctn)) vars |
21 val nvars = map (Var o ((apfst o apfst) fnctn)) vars |