40 fun add_syntax thy = |
40 fun add_syntax thy = |
41 thy |
41 thy |
42 |> Theory.copy |
42 |> Theory.copy |
43 |> Theory.root_path |
43 |> Theory.root_path |
44 |> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)] |
44 |> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)] |
45 |> Theory.add_arities [("Type", [], "logic"), ("Null", [], "logic")] |
|
46 |> Theory.add_consts |
45 |> Theory.add_consts |
47 [("typeof", "'b::logic => Type", NoSyn), |
46 [("typeof", "'b::{} => Type", NoSyn), |
48 ("Type", "'a::logic itself => Type", NoSyn), |
47 ("Type", "'a::{} itself => Type", NoSyn), |
49 ("Null", "Null", NoSyn), |
48 ("Null", "Null", NoSyn), |
50 ("realizes", "'a::logic => 'b::logic => 'b", NoSyn)]; |
49 ("realizes", "'a::{} => 'b::{} => 'b", NoSyn)]; |
51 |
50 |
52 val nullT = Type ("Null", []); |
51 val nullT = Type ("Null", []); |
53 val nullt = Const ("Null", nullT); |
52 val nullt = Const ("Null", nullT); |
54 |
53 |
55 fun mk_typ T = |
54 fun mk_typ T = |