equal
deleted
inserted
replaced
36 (* number *) |
36 (* number *) |
37 |
37 |
38 local |
38 local |
39 |
39 |
40 val zero = @{cpat "0"}; |
40 val zero = @{cpat "0"}; |
41 val zeroT = Thm.ctyp_of_term zero; |
41 val zeroT = Thm.ctyp_of_cterm zero; |
42 |
42 |
43 val one = @{cpat "1"}; |
43 val one = @{cpat "1"}; |
44 val oneT = Thm.ctyp_of_term 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.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral))); |
47 val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral)); |
48 |
48 |
49 val uminus = @{cpat "uminus"}; |
49 val uminus = @{cpat "uminus"}; |
50 val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term uminus))); |
50 val uminusT = Thm.ctyp_of @{theory} (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 |