equal
deleted
inserted
replaced
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 name_term_pairs thms thy = |
46 let |
46 let |
47 val lthy = |
47 val lthy = |
48 Theory_Target.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 val (_, lthy') = qconst_defs qtys name_term_pairs lthy; |
50 val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; |
50 val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; |
51 fun tac _ = |
51 fun tac _ = |
52 Class.intro_classes_tac [] THEN |
52 Class.intro_classes_tac [] THEN |
53 (ALLGOALS (resolve_tac lifted_thms)) |
53 (ALLGOALS (resolve_tac lifted_thms)) |