equal
deleted
inserted
replaced
42 |
42 |
43 val one = @{cpat "1"}; |
43 val one = @{cpat "1"}; |
44 val oneT = Thm.ctyp_of_cterm one; |
44 val oneT = Thm.ctyp_of_cterm one; |
45 |
45 |
46 val numeral = @{cpat "numeral"}; |
46 val numeral = @{cpat "numeral"}; |
47 val numeralT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral)); |
47 val numeralT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm numeral)); |
48 |
48 |
49 val uminus = @{cpat "uminus"}; |
49 val uminus = @{cpat "uminus"}; |
50 val uminusT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm uminus)); |
50 val uminusT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm uminus)); |
51 |
51 |
52 fun instT T V = Thm.instantiate_cterm ([(V, T)], []); |
52 fun instT T V = Thm.instantiate_cterm ([(V, T)], []); |
53 |
53 |
54 in |
54 in |
55 |
55 |