Theory.theory --> theory, Library.option --> option, Some/None-->SOME/NONE in all files
1.1 --- a/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 15:02:06 2010 +0200
1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 15:20:53 2010 +0200
1.3 @@ -38,13 +38,11 @@
1.4 use "ME/generate.sml"
1.5
1.6 ML {*
1.7 -subtract op = [1,2,3,4,5] [4,5,6,7];
1.8 -subtract op = [4,5,6,7] [1,2,3,4,5];
1.9 +SOME 111;
1.10 *}
1.11
1.12 +(*
1.13 use "ME/calchead.sml"
1.14 -
1.15 -(*
1.16 use "ME/appl.sml"
1.17 use "ME/rewtools.sml"
1.18 use "ME/script.sml"
2.1 --- a/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:02:06 2010 +0200
2.2 +++ b/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:20:53 2010 +0200
2.3 @@ -16,7 +16,7 @@
2.4 val all_modspec : ptree * pos' -> ptree * pos'
2.5 datatype appl = Appl of tac_ | Notappl of string
2.6 val appl_add :
2.7 - Theory.theory ->
2.8 + theory ->
2.9 string ->
2.10 SpecifyTools.ori list ->
2.11 SpecifyTools.itm list ->
2.12 @@ -25,9 +25,9 @@
2.13 type calcstate'
2.14 val chk_vars : Thm.cterm SpecifyTools.ppc -> string * Term.term list
2.15 val chktyp :
2.16 - Theory.theory -> int * Thm.cterm list * Thm.cterm list -> Thm.cterm
2.17 + theory -> int * Thm.cterm list * Thm.cterm list -> Thm.cterm
2.18 val chktyps :
2.19 - Theory.theory -> Thm.cterm list * Thm.cterm list -> Thm.cterm list
2.20 + theory -> Thm.cterm list * Thm.cterm list -> Thm.cterm list
2.21 val complete_metitms :
2.22 SpecifyTools.ori list ->
2.23 SpecifyTools.itm list ->
2.24 @@ -49,7 +49,7 @@
2.25 'e * 'f * 'g * Term.term * 'h -> bool
2.26 val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool
2.27 val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool
2.28 - val f_mout : Theory.theory -> mout -> Term.term
2.29 + val f_mout : theory -> mout -> Term.term
2.30 val filter_outs :
2.31 SpecifyTools.ori list ->
2.32 SpecifyTools.itm list -> SpecifyTools.ori list
2.33 @@ -71,13 +71,13 @@
2.34 val get_ocalhd : ptree * pos' -> ocalhd
2.35 val get_spec_form : tac_ -> pos' -> ptree -> mout
2.36 val geti_ct :
2.37 - Theory.theory ->
2.38 + theory ->
2.39 SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'
2.40 - val getr_ct : Theory.theory -> SpecifyTools.ori -> string * cterm'
2.41 + val getr_ct : theory -> SpecifyTools.ori -> string * cterm'
2.42 val has_list_type : Term.term -> bool
2.43 val header : pos_ -> pblID -> metID -> pblmet
2.44 val insert_ppc :
2.45 - Theory.theory ->
2.46 + theory ->
2.47 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
2.48 SpecifyTools.itm list -> SpecifyTools.itm list
2.49 val insert_ppc' :
2.50 @@ -91,13 +91,13 @@
2.51 val is_error : SpecifyTools.itm_ -> bool
2.52 val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
2.53 val is_known :
2.54 - Theory.theory ->
2.55 + theory ->
2.56 string ->
2.57 SpecifyTools.ori list ->
2.58 Term.term -> string * SpecifyTools.ori * Term.term list
2.59 val is_list_type : Term.typ -> bool
2.60 val is_notyet_input :
2.61 - Theory.theory ->
2.62 + theory ->
2.63 SpecifyTools.itm list ->
2.64 Term.term list ->
2.65 SpecifyTools.ori ->
2.66 @@ -105,25 +105,25 @@
2.67 val is_parsed : SpecifyTools.itm_ -> bool
2.68 val is_untouched : SpecifyTools.itm -> bool
2.69 val matc :
2.70 - Theory.theory ->
2.71 + theory ->
2.72 pat list ->
2.73 Term.term list ->
2.74 (int list * string * Term.term * Term.term list) list ->
2.75 (int list * string * Term.term * Term.term list) list
2.76 val match_ags :
2.77 - Theory.theory -> pat list -> Term.term list -> SpecifyTools.ori list
2.78 + theory -> pat list -> Term.term list -> SpecifyTools.ori list
2.79 val maxl : int list -> int
2.80 val match_ags_msg : string list -> Term.term -> Term.term list -> unit
2.81 val memI : ''a list -> ''a -> bool
2.82 val mk_additem : string -> cterm' -> tac
2.83 - val mk_delete : Theory.theory -> string -> SpecifyTools.itm_ -> tac
2.84 + val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
2.85 val mtc :
2.86 - Theory.theory -> pat -> Term.term -> SpecifyTools.preori Library.option
2.87 + theory -> pat -> Term.term -> SpecifyTools.preori option
2.88 val nxt_add :
2.89 - Theory.theory ->
2.90 + theory ->
2.91 SpecifyTools.ori list ->
2.92 (string * (Term.term * 'a)) list ->
2.93 - SpecifyTools.itm list -> (string * cterm') Library.option
2.94 + SpecifyTools.itm list -> (string * cterm') option
2.95 val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
2.96 val nxt_spec :
2.97 pos_ ->
2.98 @@ -147,7 +147,7 @@
2.99 SpecifyTools.itm_ ->
2.100 Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
2.101 val overwrite_ppc :
2.102 - Theory.theory ->
2.103 + theory ->
2.104 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
2.105 SpecifyTools.itm list ->
2.106 (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
2.107 @@ -159,24 +159,24 @@
2.108 val ppc2list : 'a SpecifyTools.ppc -> 'a list
2.109 val pt_extract :
2.110 ptree * (int list * pos_) ->
2.111 - ptform * tac Library.option * Term.term list
2.112 + ptform * tac option * Term.term list
2.113 val pt_form : ppobj -> ptform
2.114 val pt_model : ppobj -> pos_ -> ptform
2.115 val reset_calchead : ptree * pos' -> ptree * pos'
2.116 val seek_oridts :
2.117 - Theory.theory ->
2.118 + theory ->
2.119 string ->
2.120 Term.term * Term.term list ->
2.121 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
2.122 -> string * SpecifyTools.ori * Term.term list
2.123 val seek_orits :
2.124 - Theory.theory ->
2.125 + theory ->
2.126 string ->
2.127 Term.term list ->
2.128 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
2.129 -> string * SpecifyTools.ori * Term.term list
2.130 val seek_ppc :
2.131 - int -> SpecifyTools.itm list -> SpecifyTools.itm Library.option
2.132 + int -> SpecifyTools.itm list -> SpecifyTools.itm option
2.133 val show_pt : ptree -> unit
2.134 val some_spec : spec -> spec -> spec
2.135 val specify :
2.136 @@ -193,8 +193,8 @@
2.137 'b ->
2.138 ptree ->
2.139 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
2.140 - val tag_form : Theory.theory -> Thm.cterm * Thm.cterm -> Thm.cterm
2.141 - val test_types : Theory.theory -> Term.term * Term.term list -> string
2.142 + val tag_form : theory -> Thm.cterm * Thm.cterm -> Thm.cterm
2.143 + val test_types : theory -> Term.term * Term.term list -> string
2.144 val typeless : Term.term -> Term.term
2.145 val unbound_ppc : Thm.cterm SpecifyTools.ppc -> Term.term list
2.146 val vals_of_oris : SpecifyTools.ori list -> Term.term list
3.1 --- a/src/Tools/isac/ME/inform.sml Thu Aug 19 15:02:06 2010 +0200
3.2 +++ b/src/Tools/isac/ME/inform.sml Thu Aug 19 15:20:53 2010 +0200
3.3 @@ -23,7 +23,7 @@
3.4 val imodel2fstr : iitem list -> (string * cterm') list
3.5
3.6
3.7 - val Isac : 'a -> Theory.theory
3.8 + val Isac : 'a -> theory
3.9 val appl_add' :
3.10 theory' ->
3.11 SpecifyTools.ori list ->
3.12 @@ -67,7 +67,7 @@
3.13 (* val filter_sep : ('a -> bool) -> 'a list -> 'a list * 'a list *)
3.14 (* val flattup2 : 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e *)
3.15 (* val fstr2itm_ :
3.16 - Theory.theory ->
3.17 + theory ->
3.18 (''a * (Term.term * Term.term)) list ->
3.19 ''a * string -> int list * bool * ''a * SpecifyTools.itm_ *)
3.20 val inform :
3.21 @@ -85,7 +85,7 @@
3.22 val oris2itms :
3.23 'a -> int -> SpecifyTools.ori list -> SpecifyTools.itm list
3.24 (* val par2fstr : SpecifyTools.itm -> string * cterm' *)
3.25 - (* val parsitm : Theory.theory -> SpecifyTools.itm -> SpecifyTools.itm *)
3.26 + (* val parsitm : theory -> SpecifyTools.itm -> SpecifyTools.itm *)
3.27 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
3.28 (* val unknown_expl :
3.29 theory' ->
4.1 --- a/src/Tools/isac/ME/mathengine.sml Thu Aug 19 15:02:06 2010 +0200
4.2 +++ b/src/Tools/isac/ME/mathengine.sml Thu Aug 19 15:20:53 2010 +0200
4.3 @@ -31,7 +31,7 @@
4.4 val detailstep : ptree -> pos' -> string * ptree * pos'
4.5 (* val e_tac_ : tac_ *)
4.6 val f2str : mout -> cterm'
4.7 - (* val get_pblID : ptree * pos' -> pblID Library.option *)
4.8 + (* val get_pblID : ptree * pos' -> pblID option *)
4.9 val initmatch : ptree -> pos' -> ptform
4.10 (* val loc_solve_ :
4.11 string * tac_ -> ptree * (int list * pos_) -> lOc_ *)
5.1 --- a/src/Tools/isac/Scripts/term_G.sml Thu Aug 19 15:02:06 2010 +0200
5.2 +++ b/src/Tools/isac/Scripts/term_G.sml Thu Aug 19 15:20:53 2010 +0200
5.3 @@ -12,7 +12,7 @@
5.4 (*1003 fun match thy t pat =
5.5 (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)))
5.6 handle _ => [];
5.7 -fn : Theory.theory ->
5.8 +fn : theory ->
5.9 Term.term -> Term.term -> (Term.indexname * Term.term) list*)
5.10 (*see src/Tools/eqsubst.ML fun clean_match*)
5.11 (*1003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*)
5.12 @@ -712,7 +712,7 @@
5.13 in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end;
5.14
5.15 fun get_thm' xstring = (*?covers 2009 Thm?!, replaces 2002 fun get_thm :
5.16 -val it = fn : Theory.theory -> xstring -> Thm.thm*)
5.17 +val it = fn : theory -> xstring -> Thm.thm*)
5.18 Thm (xstring,
5.19 num_str (ProofContext.get_thm (thy2ctxt' "Isac") xstring));
5.20