adbrucker
/
isabelle-hacks
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Support type synonyms as input notation.

This commit is contained in:
Achim D. Brucker 2018-06-18 13:32:18 +01:00
parent 3b0a88dfa6
commit 8e9a19266a
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Hiding_Type_Variables.thy
View File

@ -177,7 +177,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
fun register typ_str print_mode parse_mode thy =
let
val ctx = Toplevel.context_of(Toplevel.theory_toplevel thy)
val typ = Syntax.read_typ ctx typ_str
val typ = Syntax.parse_typ ctx typ_str
val (name,tvars) = case typ of
Type(name,ts) => let
val tvars = map (fn (TFree(n,_)) => n
@ -259,6 +259,7 @@ assert[string_of_thm_equal,
str="g (a::('a + 'b, 'a \<times> 'b) foobar) (b::('a + 'b, 'a \<times> 'b) foobar) = a"]
register_default_tvars "('alpha, 'beta) foobar" (always,active)
register_default_tvars "('alpha, 'beta, 'gamma, 'delta) baz" (always,active)
update_default_tvars_mode "_ foobar" (noprint,noparse)
assert[string_of_thm_equal,
@ -285,4 +286,8 @@ definition A :: "'alpha \<Rightarrow> __ foobar"
definition B :: "__ foobar \<Rightarrow> __ foobar \<Rightarrow> __ foobar"
where "B x y = x"
definition C :: "__ baz \<Rightarrow> __ foobar \<Rightarrow> __ baz"
where "C x y = x"
end