equal
deleted
inserted
replaced
96 *} |
96 *} |
97 |
97 |
98 (* A test whether get_fun works properly |
98 (* A test whether get_fun works properly |
99 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t" |
99 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t" |
100 local_setup {* |
100 local_setup {* |
101 fn lthy => (Toplevel.program (fn () => |
101 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |> snd |
102 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
|
103 )) |> snd |
|
104 *} |
102 *} |
105 *) |
103 *) |
106 |
104 |
107 consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
105 consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
108 axioms Rl_eq: "EQUIV Rl" |
106 axioms Rl_eq: "EQUIV Rl" |