merge
This commit is contained in:
parent
f7dc9e7247
commit
592f6b564a
|
@ -669,11 +669,11 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
|
|||
(Cmd.interpretation1 n loc_n loc_param))
|
||||
|>:: terminal_proof_dual top o_by)
|
||||
| Theory_hide_const hide_const =>
|
||||
cons (@{command_keyword hide_const}, Cmd.hide_const top hide_const)
|
||||
cons (\<^command_keyword>\<open>hide_const\<close>, Cmd.hide_const top hide_const)
|
||||
| Theory_abbreviation abbreviation =>
|
||||
cons (@{command_keyword abbreviation}, Cmd.abbreviation top abbreviation)
|
||||
cons (\<^command_keyword>\<open>abbreviation\<close>, Cmd.abbreviation top abbreviation)
|
||||
| Theory_code_reflect code_reflect' =>
|
||||
cons (@{command_keyword code_reflect'}, Cmd.code_reflect' top code_reflect')
|
||||
cons (\<^command_keyword>\<open>code_reflect'\<close>, Cmd.code_reflect' top code_reflect')
|
||||
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
|
||||
end*)
|
||||
end
|
||||
|
|
|
@ -658,11 +658,11 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
|
|||
(Cmd.interpretation1 n loc_n loc_param))
|
||||
|>:: terminal_proof_dual top o_by)
|
||||
| Theory_hide_const hide_const =>
|
||||
cons (@{command_keyword hide_const}, Cmd.hide_const top hide_const)
|
||||
cons (\<^command_keyword>\<open>hide_const\<close>, Cmd.hide_const top hide_const)
|
||||
| Theory_abbreviation abbreviation =>
|
||||
cons (@{command_keyword abbreviation}, Cmd.abbreviation top abbreviation)
|
||||
cons (\<^command_keyword>\<open>abbreviation\<close>, Cmd.abbreviation top abbreviation)
|
||||
| Theory_code_reflect code_reflect' =>
|
||||
cons (@{command_keyword code_reflect'}, Cmd.code_reflect' top code_reflect')
|
||||
cons (\<^command_keyword>\<open>code_reflect'\<close>, Cmd.code_reflect' top code_reflect')
|
||||
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
|
||||
end*)
|
||||
end
|
||||
|
|
|
@ -702,11 +702,11 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
|
|||
(Cmd.interpretation1 n loc_n loc_param))
|
||||
|>:: terminal_proof_dual top o_by)
|
||||
| Theory_hide_const hide_const =>
|
||||
cons (@{command_keyword hide_const}, Cmd.hide_const top hide_const)
|
||||
cons (\<^command_keyword>\<open>hide_const\<close>, Cmd.hide_const top hide_const)
|
||||
| Theory_abbreviation abbreviation =>
|
||||
cons (@{command_keyword abbreviation}, Cmd.abbreviation top abbreviation)
|
||||
cons (\<^command_keyword>\<open>abbreviation\<close>, Cmd.abbreviation top abbreviation)
|
||||
| Theory_code_reflect code_reflect' =>
|
||||
cons (@{command_keyword code_reflect'}, Cmd.code_reflect' top code_reflect')
|
||||
cons (\<^command_keyword>\<open>code_reflect'\<close>, Cmd.code_reflect' top code_reflect')
|
||||
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
|
||||
end*)
|
||||
end
|
||||
|
|
|
@ -677,11 +677,11 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
|
|||
(Cmd.interpretation1 n loc_n loc_param))
|
||||
|>:: terminal_proof_dual top o_by)
|
||||
| Theory_hide_const hide_const =>
|
||||
cons (@{command_keyword hide_const}, Cmd.hide_const top hide_const)
|
||||
cons (\<^command_keyword>\<open>hide_const\<close>, Cmd.hide_const top hide_const)
|
||||
| Theory_abbreviation abbreviation =>
|
||||
cons (@{command_keyword abbreviation}, Cmd.abbreviation top abbreviation)
|
||||
cons (\<^command_keyword>\<open>abbreviation\<close>, Cmd.abbreviation top abbreviation)
|
||||
| Theory_code_reflect code_reflect' =>
|
||||
cons (@{command_keyword code_reflect'}, Cmd.code_reflect' top code_reflect')
|
||||
cons (\<^command_keyword>\<open>code_reflect'\<close>, Cmd.code_reflect' top code_reflect')
|
||||
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
|
||||
end*)
|
||||
end
|
||||
|
|
Loading…
Reference in New Issue