tuned signature
authorhaftmann
Mon Jun 06 21:28:46 2016 +0200 (2016-06-06)
changeset 63241f59fd6cc935e
parent 63240 f82c0b803bda
child 63242 9986559617ee
child 63243 1bc6816fd525
child 63249 d1693d7b0c01
tuned signature
src/Doc/Codegen/Further.thy
src/Pure/Isar/code.ML
     1.1 --- a/src/Doc/Codegen/Further.thy	Mon Jun 06 21:28:46 2016 +0200
     1.2 +++ b/src/Doc/Codegen/Further.thy	Mon Jun 06 21:28:46 2016 +0200
     1.3 @@ -345,4 +345,3 @@
     1.4  \<close>
     1.5  
     1.6  end
     1.7 -
     2.1 --- a/src/Pure/Isar/code.ML	Mon Jun 06 21:28:46 2016 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Mon Jun 06 21:28:46 2016 +0200
     2.3 @@ -10,10 +10,8 @@
     2.4  sig
     2.5    (*constants*)
     2.6    val check_const: theory -> term -> string
     2.7 -  val read_bare_const: theory -> string -> string * typ
     2.8    val read_const: theory -> string -> string
     2.9    val string_of_const: theory -> string -> string
    2.10 -  val const_typ: theory -> string -> typ
    2.11    val args_number: theory -> string -> int
    2.12  
    2.13    (*constructor sets*)
    2.14 @@ -21,12 +19,8 @@
    2.15      -> string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
    2.16  
    2.17    (*code equations and certificates*)
    2.18 -  val mk_eqn: theory -> thm * bool -> thm * bool
    2.19 -  val mk_eqn_liberal: theory -> thm -> (thm * bool) option
    2.20    val assert_eqn: theory -> thm * bool -> thm * bool
    2.21    val assert_abs_eqn: theory -> string option -> thm -> thm * string
    2.22 -  val const_typ_eqn: theory -> thm -> string * typ
    2.23 -  val expand_eta: theory -> int -> thm -> thm
    2.24    type cert
    2.25    val constrain_cert: theory -> sort list -> cert -> cert
    2.26    val conclude_cert: cert -> cert