equal
deleted
inserted
replaced
40 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
40 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
41 end |
41 end |
42 |
42 |
43 |
43 |
44 (* defines the quotient permutations *) |
44 (* defines the quotient permutations *) |
45 fun qperm_defs qtys full_tnames name_term_pairs thms thy = |
45 fun qperm_defs qtys full_tnames perm_specs thms thy = |
46 let |
46 let |
47 val lthy = |
47 val lthy = |
48 Class.instantiation (full_tnames, [], @{sort pt}) thy; |
48 Class.instantiation (full_tnames, [], @{sort pt}) thy; |
49 val (_, lthy') = qconst_defs qtys name_term_pairs lthy; |
49 |
|
50 val (_, lthy') = qconst_defs qtys perm_specs lthy; |
|
51 |
50 val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; |
52 val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; |
|
53 |
51 fun tac _ = |
54 fun tac _ = |
52 Class.intro_classes_tac [] THEN |
55 Class.intro_classes_tac [] THEN |
53 (ALLGOALS (resolve_tac lifted_thms)) |
56 (ALLGOALS (resolve_tac lifted_thms)) |
54 val lthy'' = Class.prove_instantiation_instance tac lthy' |
|
55 in |
57 in |
56 Local_Theory.exit_global lthy'' |
58 lthy' |
|
59 |> Class.prove_instantiation_exit tac |
57 end |
60 end |
58 |
61 |
59 |
62 |
60 end (* structure *) |
63 end (* structure *) |
61 |
64 |