forked from Isabelle_DOF/Isabelle_DOF
corrected and re-inserted Ecclectic Man into build
This commit is contained in:
parent
3e99e9e013
commit
2351e00be6
|
@ -1,2 +1,2 @@
|
|||
Isabelle_DOF-Manual
|
||||
#TR_my_commented_isabelle
|
||||
TR_my_commented_isabelle
|
||||
|
|
|
@ -628,19 +628,20 @@ text\<open>
|
|||
text \<open>Apparently, a bizarre conversion between the old-style interface and
|
||||
the new-style \<^ML>\<open>tyenv\<close> is necessary. See the following example.\<close>
|
||||
ML\<open>
|
||||
val S = Vartab.dest tyenv;
|
||||
val S = Vartab.dest tyenv : (Vartab.key * (sort * typ)) list;
|
||||
val S' = (map (fn (s,(t,u)) => ((s,t),u)) S) : ((indexname * sort) * typ) list;
|
||||
(* it took me quite some time to find out that these two type representations,
|
||||
obscured by a number of type-synonyms, where actually identical. *)
|
||||
val S''= TVars.make S': typ TVars.table
|
||||
val ty = t_schematic;
|
||||
val ty' = Term_Subst.instantiateT S' t_schematic;
|
||||
val ty' = Term_Subst.instantiateT S'' t_schematic;
|
||||
|
||||
(* Don't know how to build a typ TVars.table *)
|
||||
val t = (generalize_term @{term "[]"});
|
||||
|
||||
val t' = Term_Subst.map_types_same (Term_Subst.instantiateT S') (t)
|
||||
val t' = Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S')) (t)
|
||||
(* or alternatively : *)
|
||||
val t'' = Term.map_types (Term_Subst.instantiateT S') (t)
|
||||
val t'' = Term.map_types (Term_Subst.instantiateT S'') (t)
|
||||
\<close>
|
||||
|
||||
text\<open>A more abstract env for variable management in tactic proofs. A bit difficult to use
|
||||
|
|
|
@ -1917,7 +1917,7 @@ fun print_item string_of (modes, arg) state =
|
|||
fun print_term meta_args_opt (string_list, string) trans =
|
||||
let
|
||||
val pos = Toplevel.pos_of trans
|
||||
fun prin state str = string_of_term str pos (Toplevel.context_of state)
|
||||
fun prin state str = string_of_term string pos (Toplevel.context_of state)
|
||||
in
|
||||
Toplevel.theory(fn thy =>
|
||||
(print_item prin (string_list, string) (Toplevel.theory_toplevel thy);
|
||||
|
|
Loading…
Reference in New Issue