1.1 --- a/doc-isac/mlehnfeld/master/Unsynchronized.ref.txt Thu Jun 26 17:19:30 2014 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,441 +0,0 @@
1.4 -neuper@neuper:/usr/local/isabisac/src$ grep -r "Unsynchronized.ref " *
1.5 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.6 -relevance for Isac's parallel math-engine: # low .. ##### high
1.7 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.8 -legend:
1.9 ---- comments
1.10 -!! to be replaced by Theory_Data
1.11 -!? to be replaced by other means
1.12 -@ first quick marks for possible relevance
1.13 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.14 -
1.15 - Doc/IsarImplementation/ML.thy: @{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\
1.16 - Doc/IsarImplementation/ML.thy: @{index_ML_op ":=": "'a Unsynchronized.ref * 'a -> unit"} \\
1.17 - FOLP/simp.ML:val tracing = Unsynchronized.ref false;
1.18 - HOL/HOLCF/Tools/Domain/domain_induction.ML:val quiet_mode = Unsynchronized.ref false
1.19 -
1.20 ---- Isac is a level deeper than HOL, at level Pure ...
1.21 - HOL/HOLCF/Tools/Domain/domain_induction.ML:val trace_domain = Unsynchronized.ref false
1.22 - HOL/Matrix_LP/Cplex_tools.ML:val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
1.23 - HOL/Matrix_LP/Cplex_tools.ML: val ignore_NL = Unsynchronized.ref true
1.24 - HOL/Matrix_LP/Cplex_tools.ML: val rest = Unsynchronized.ref []
1.25 - HOL/Matrix_LP/Cplex_tools.ML: val linebuf = Unsynchronized.ref ""
1.26 - HOL/Matrix_LP/Cplex_tools.ML: val rest = Unsynchronized.ref []
1.27 - HOL/Matrix_LP/Cplex_tools.ML: val rest = Unsynchronized.ref []
1.28 - HOL/Matrix_LP/FloatSparseMatrixBuilder.ML: val ytable = Unsynchronized.ref Inttab.empty
1.29 - HOL/Matrix_LP/FloatSparseMatrixBuilder.ML: val count = Unsynchronized.ref 0;
1.30 - HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML:val max_reductions = Unsynchronized.ref (NONE : int option)
1.31 - HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML: val s = Unsynchronized.ref (Continue p)
1.32 - HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML: val counter = Unsynchronized.ref 0
1.33 - HOL/Matrix_LP/Compute_Oracle/compute.ML: (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming)
1.34 - HOL/Matrix_LP/Compute_Oracle/compute.ML:fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy
1.35 - HOL/Matrix_LP/Compute_Oracle/compute.ML:fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps
1.36 - HOL/Matrix_LP/Compute_Oracle/compute.ML:fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable)
1.37 - HOL/Matrix_LP/Compute_Oracle/compute.ML:fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable
1.38 - HOL/Matrix_LP/Compute_Oracle/compute.ML:fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
1.39 - HOL/Matrix_LP/Compute_Oracle/compute.ML:fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog
1.40 - HOL/Matrix_LP/Compute_Oracle/compute.ML:fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
1.41 - HOL/Matrix_LP/Compute_Oracle/compute.ML:fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,_,p2,p3,p4,p5,p6)))) encoding' =
1.42 - HOL/Matrix_LP/Compute_Oracle/compute.ML:fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n
1.43 - HOL/Matrix_LP/Compute_Oracle/compute.ML:fun set_naming (Computer (r as Unsynchronized.ref (SOME (p1,p2,p3,p4,p5,p6,_)))) naming'=
1.44 - HOL/Matrix_LP/Compute_Oracle/compute.ML: Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms)))
1.45 - HOL/Matrix_LP/Compute_Oracle/compute.ML:datatype theorem = Theorem of theory_ref * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table
1.46 - HOL/Matrix_LP/Compute_Oracle/am_sml.ML: val dump_output : (string option) Unsynchronized.ref
1.47 - HOL/Matrix_LP/Compute_Oracle/am_sml.ML:val dump_output = Unsynchronized.ref (NONE: string option)
1.48 - HOL/Matrix_LP/Compute_Oracle/am_sml.ML:val saved_result = Unsynchronized.ref (NONE:(string*term)option)
1.49 - HOL/Matrix_LP/Compute_Oracle/am_sml.ML:val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
1.50 - HOL/Matrix_LP/Compute_Oracle/am_sml.ML: val buffer = Unsynchronized.ref ""
1.51 - HOL/Matrix_LP/Compute_Oracle/am_sml.ML:val guid_counter = Unsynchronized.ref 0
1.52 - HOL/Matrix_LP/Compute_Oracle/linker.ML: PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref *
1.53 - HOL/Matrix_LP/Compute_Oracle/linker.ML: pattern list Unsynchronized.ref
1.54 - HOL/Matrix_LP/Compute_Oracle/linker.ML: val changed = Unsynchronized.ref false
1.55 - HOL/Matrix_LP/Compute_Oracle/linker.ML: val counter = Unsynchronized.ref 0
1.56 - HOL/Matrix_LP/Compute_Oracle/linker.ML: val tab = Unsynchronized.ref (CThmtab.empty : unit CThmtab.table)
1.57 - HOL/Matrix_LP/Compute_Oracle/linker.ML: val thstab = Unsynchronized.ref (Inttab.empty : thm Inttab.table)
1.58 - HOL/Matrix_LP/Compute_Oracle/linker.ML: PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats)
1.59 - HOL/Matrix_LP/Compute_Oracle/am_compiler.ML:val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
1.60 - HOL/Matrix_LP/Compute_Oracle/am_compiler.ML: val buffer = Unsynchronized.ref ""
1.61 - HOL/Matrix_LP/Compute_Oracle/am_compiler.ML: " val s = Unsynchronized.ref (Continue p)",
1.62 - HOL/Matrix_LP/Compute_Oracle/am_ghc.ML: val buffer = Unsynchronized.ref ""
1.63 - HOL/Matrix_LP/Compute_Oracle/am_ghc.ML:val guid_counter = Unsynchronized.ref 0
1.64 - HOL/Matrix_LP/Compute_Oracle/report.ML: val report_depth = Unsynchronized.ref 0
1.65 - HOL/Random.thy:val seed = Unsynchronized.ref
1.66 - HOL/Mutabelle/mutabelle_extra.ML:val random_seed = Unsynchronized.ref 1.0;
1.67 - HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML:val data = Unsynchronized.ref ([] : (int * data) list)
1.68 - HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML:val num_sledgehammer_calls = Unsynchronized.ref 0
1.69 - HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML: val reconstructor = Unsynchronized.ref ""
1.70 - HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML: Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
1.71 - HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val proof_table = Unsynchronized.ref (Prooftab.empty: string list list Prooftab.table)
1.72 - HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_successes = Unsynchronized.ref ([] : (int * int) list)
1.73 - HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_failures = Unsynchronized.ref ([] : (int * int) list)
1.74 - HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_found_proofs = Unsynchronized.ref ([] : (int * int) list)
1.75 - HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_lost_proofs = Unsynchronized.ref ([] : (int * int) list)
1.76 - HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_found_facts = Unsynchronized.ref ([] : (int * int) list)
1.77 - HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_lost_facts = Unsynchronized.ref ([] : (int * int) list)
1.78 - HOL/Statespace/DistinctTreeProver.thy:val da = Unsynchronized.ref refl;
1.79 - HOL/Tools/try0.ML:val auto = Unsynchronized.ref false
1.80 - HOL/Tools/Function/scnp_solve.ML:val solver = Unsynchronized.ref "auto";
1.81 - HOL/Tools/Function/function_core.ML:val trace = Unsynchronized.ref false
1.82 - HOL/Tools/Function/function_common.ML:val profile = Unsynchronized.ref false;
1.83 - HOL/Tools/sat_funcs.ML: val trace_sat: bool Unsynchronized.ref (* input: print trace messages *)
1.84 - HOL/Tools/sat_funcs.ML: val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *)
1.85 - HOL/Tools/sat_funcs.ML: val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *)
1.86 - HOL/Tools/sat_funcs.ML:val trace_sat = Unsynchronized.ref false;
1.87 - HOL/Tools/sat_funcs.ML:val solver = Unsynchronized.ref "zchaff_with_proofs";
1.88 - HOL/Tools/sat_funcs.ML:val counter = Unsynchronized.ref 0;
1.89 - HOL/Tools/Sledgehammer/sledgehammer_provers.ML:val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
1.90 - HOL/Tools/Sledgehammer/sledgehammer_isar.ML:val auto = Unsynchronized.ref false
1.91 - HOL/Tools/Sledgehammer/sledgehammer_isar.ML:val provers = Unsynchronized.ref ""
1.92 - HOL/Tools/Sledgehammer/sledgehammer_isar.ML:val timeout = Unsynchronized.ref 30
1.93 - HOL/Tools/Nitpick/nitpick.ML: val state_ref = Unsynchronized.ref state
1.94 - HOL/Tools/Nitpick/nitpick.ML: val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
1.95 - HOL/Tools/Nitpick/nitpick.ML: ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
1.96 - HOL/Tools/Nitpick/nitpick.ML: special_funs = Unsynchronized.ref [],
1.97 - HOL/Tools/Nitpick/nitpick.ML: unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
1.98 - HOL/Tools/Nitpick/nitpick.ML: constr_cache = Unsynchronized.ref []}
1.99 - HOL/Tools/Nitpick/nitpick.ML: val too_big_scopes = Unsynchronized.ref []
1.100 - HOL/Tools/Nitpick/nitpick.ML: val scopes = Unsynchronized.ref []
1.101 - HOL/Tools/Nitpick/nitpick.ML: val generated_scopes = Unsynchronized.ref []
1.102 - HOL/Tools/Nitpick/nitpick.ML: val generated_problems = Unsynchronized.ref ([] : rich_problem list)
1.103 - HOL/Tools/Nitpick/nitpick.ML: val checked_problems = Unsynchronized.ref (SOME [])
1.104 - HOL/Tools/Nitpick/nitpick.ML: val met_potential = Unsynchronized.ref 0
1.105 - HOL/Tools/Nitpick/nitpick_hol.ML: val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
1.106 - HOL/Tools/Nitpick/nitpick_mono.ML:val trace = Unsynchronized.ref false
1.107 - HOL/Tools/Nitpick/nitpick_mono.ML: max_fresh = Unsynchronized.ref 0, datatype_mcache = Unsynchronized.ref [],
1.108 - HOL/Tools/Nitpick/nitpick_mono.ML: constr_mcache = Unsynchronized.ref []} : mdata)
1.109 - HOL/Tools/Nitpick/kodkod.ML:val created_temp_dir = Unsynchronized.ref false
1.110 - HOL/Tools/Nitpick/kodkod.ML: val in_buf = Unsynchronized.ref Buffer.empty
1.111 - HOL/Tools/Nitpick/nitpick_isar.ML:val auto = Unsynchronized.ref false
1.112 - HOL/Tools/Nitpick/nitpick_model.ML: val pool = Unsynchronized.ref []
1.113 - HOL/Tools/Nitpick/nitpick_model.ML: val pool = Unsynchronized.ref []
1.114 - HOL/Tools/Meson/meson.ML: let val ctxt0r = Unsynchronized.ref ctxt0 (* FIXME ??? *)
1.115 - HOL/Tools/Quickcheck/random_generators.ML: val state = Unsynchronized.ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
1.116 - HOL/Tools/Quickcheck/narrowing_generators.ML: val current_size = Unsynchronized.ref 0
1.117 - HOL/Tools/Quickcheck/narrowing_generators.ML: val current_result = Unsynchronized.ref Quickcheck.empty_result
1.118 - HOL/Tools/Quickcheck/quickcheck_common.ML: val current_size = Unsynchronized.ref 0
1.119 - HOL/Tools/Quickcheck/quickcheck_common.ML: val current_result = Unsynchronized.ref Quickcheck.empty_result
1.120 - HOL/Tools/Quickcheck/quickcheck_common.ML: val current_result = Unsynchronized.ref Quickcheck.empty_result
1.121 - HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML:val nrandom = Unsynchronized.ref 3;
1.122 - HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML:val debug = Unsynchronized.ref false;
1.123 - HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML:val no_higher_order_predicate = Unsynchronized.ref ([] : string list);
1.124 - HOL/Tools/Predicate_Compile/predicate_compile.ML:val present_graph = Unsynchronized.ref false
1.125 - HOL/Tools/Predicate_Compile/predicate_compile.ML:val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref
1.126 - HOL/Tools/Predicate_Compile/code_prolog.ML:val trace = Unsynchronized.ref false
1.127 - HOL/Tools/sat_solver.ML: val solvers = Unsynchronized.ref ([] : (string * solver) list);
1.128 - HOL/Tools/sat_solver.ML: val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1)
1.129 - HOL/Tools/sat_solver.ML: val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
1.130 - HOL/Tools/sat_solver.ML: val empty_id = Unsynchronized.ref ~1
1.131 - HOL/Tools/sat_solver.ML: val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table)
1.132 - HOL/Tools/sat_solver.ML: val next_id = Unsynchronized.ref (number_of_clauses - 1)
1.133 - HOL/Tools/sat_solver.ML: val clause_offset = Unsynchronized.ref ~1
1.134 - HOL/Tools/sat_solver.ML: val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
1.135 - HOL/Tools/sat_solver.ML: val empty_id = Unsynchronized.ref ~1
1.136 - HOL/Tools/prop_logic.ML: val new = Unsynchronized.ref (maxidx fm' + 1)
1.137 - HOL/Tools/prop_logic.ML: val next_idx_is_valid = Unsynchronized.ref false
1.138 - HOL/Tools/prop_logic.ML: val next_idx = Unsynchronized.ref 0
1.139 - HOL/Tools/TFL/rules.ML:val tracing = Unsynchronized.ref false;
1.140 - HOL/Tools/TFL/rules.ML: val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
1.141 - HOL/Tools/TFL/tfl.ML:val trace = Unsynchronized.ref false;
1.142 - HOL/Tools/TFL/tfl.ML: let val slist = Unsynchronized.ref names
1.143 - HOL/Tools/TFL/tfl.ML: val vname = Unsynchronized.ref "u"
1.144 - HOL/Tools/cnf_funcs.ML: val var_id = Unsynchronized.ref 0 (* properly initialized below *)
1.145 - HOL/TPTP/TPTP_Parser/tptp_parser.ML: val currentPos = Unsynchronized.ref 0
1.146 - HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML: datatype 'a str = EVAL of 'a * 'a str Unsynchronized.ref | UNEVAL of (unit->'a)
1.147 - HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML:val col = Unsynchronized.ref 0;
1.148 - HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML:val linep = Unsynchronized.ref 1; (* Line pointer *)
1.149 - HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML:val eolpos = Unsynchronized.ref 0;
1.150 - HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yyb = Unsynchronized.ref "\n" (* buffer *)
1.151 - HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yybl = Unsynchronized.ref 1 (*buffer length *)
1.152 - HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yybufpos = Unsynchronized.ref 1 (* location of next character to use *)
1.153 - HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yygone = Unsynchronized.ref yygone0 (* position in file of beginning of buffer *)
1.154 - HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yydone = Unsynchronized.ref false (* eof found yet? *)
1.155 - HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yybegin = Unsynchronized.ref 1 (*Current 'start state' for lexer *)
1.156 - HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML:val s = Unsynchronized.ref "" and index = Unsynchronized.ref 0
1.157 - HOL/Decision_Procs/cooper_tac.ML:val trace = Unsynchronized.ref false;
1.158 - HOL/Decision_Procs/mir_tac.ML:val trace = Unsynchronized.ref false;
1.159 - HOL/Decision_Procs/ferrack_tac.ML:val trace = Unsynchronized.ref false;
1.160 - HOL/Nitpick_Examples/Mono_Nits.thy:val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
1.161 - HOL/Nitpick_Examples/Mono_Nits.thy: skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
1.162 - HOL/Nitpick_Examples/Mono_Nits.thy: unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
1.163 - HOL/Nitpick_Examples/Mono_Nits.thy: constr_cache = Unsynchronized.ref []}
1.164 - HOL/ex/SVC_Oracle.thy: val vname = Unsynchronized.ref "V_a"
1.165 - HOL/ex/SVC_Oracle.thy: val pairs = Unsynchronized.ref ([] : (term*term) list)
1.166 - HOL/ex/svc_funcs.ML: val trace = Unsynchronized.ref false;
1.167 - HOL/ex/svc_funcs.ML: val nat_vars = Unsynchronized.ref ([] : string list)
1.168 -
1.169 ---- Provers are an internal part of Isabelle, where Isac should not conflict with
1.170 - Provers/blast.ML: | Skolem of string * term option Unsynchronized.ref list
1.171 - Provers/blast.ML: | Skolem of string * term option Unsynchronized.ref list
1.172 - Provers/blast.ML: vars: term option Unsynchronized.ref list, (*variables occurring in branch*)
1.173 - Provers/blast.ML: trail: term option Unsynchronized.ref list Unsynchronized.ref,
1.174 - Provers/blast.ML: names = Unsynchronized.ref (Variable.names_of ctxt),
1.175 - Provers/blast.ML: fullTrace = Unsynchronized.ref [],
1.176 - Provers/blast.ML: trail = Unsynchronized.ref [],
1.177 - Provers/blast.ML: ntrail = Unsynchronized.ref 0,
1.178 - Provers/blast.ML: nclosed = Unsynchronized.ref 0, (*number of branches closed during the search*)
1.179 - Provers/blast.ML: ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*)
1.180 - Provers/blast.ML: NONE => let val t' = Var (Unsynchronized.ref NONE)
1.181 - Provers/blast.ML: | t aconv (Var (Unsynchronized.ref (SOME u))) = t aconv u
1.182 - Provers/blast.ML: | add_term_vars (Var (v as Unsynchronized.ref NONE), vars) = ins_var (v, vars)
1.183 - Provers/blast.ML: | add_term_vars (Var (Unsynchronized.ref (SOME u)), vars) = add_term_vars (u, vars)
1.184 - Provers/blast.ML: | add_vars_vars (Unsynchronized.ref (SOME u) :: vs, vars) =
1.185 - Provers/blast.ML: | (Var (Unsynchronized.ref NONE)) => t
1.186 - Provers/blast.ML: | (Var (Unsynchronized.ref (SOME u))) => norm u
1.187 - Provers/blast.ML: let val alistVar = Unsynchronized.ref []
1.188 - Provers/blast.ML: and alistTVar = Unsynchronized.ref []
1.189 - Provers/blast.ML: NONE => let val t' = Var (Unsynchronized.ref NONE)
1.190 - Provers/blast.ML: let val name = Unsynchronized.ref "a"
1.191 - Provers/blast.ML: val updated = Unsynchronized.ref []
1.192 - Provers/blast.ML: | inst (Var(v as Unsynchronized.ref NONE)) = (updated := v :: (!updated);
1.193 - Provers/blast.ML: Const (c, _) $ Var (Unsynchronized.ref (SOME (Const ("*False*", _)))) =>
1.194 - Provers/blast.ML: | showTerm d (Var (Unsynchronized.ref NONE)) = dummyVar2
1.195 - Provers/blast.ML: val alistVar = Unsynchronized.ref []
1.196 - Provers/blast.ML: and alistTVar = Unsynchronized.ref []
1.197 - Provers/blast.ML: NONE => (alistVar := (ix, (Unsynchronized.ref NONE, bounds ts))
1.198 - Provers/trancl.ML: val pred = Unsynchronized.ref [];
1.199 - Provers/trancl.ML: val visited = Unsynchronized.ref [];
1.200 - Provers/trancl.ML: val visited = Unsynchronized.ref [];
1.201 - Provers/quasi.ML: val pred = Unsynchronized.ref [];
1.202 - Provers/quasi.ML: val visited = Unsynchronized.ref [];
1.203 - Provers/order.ML: val finish : term list Unsynchronized.ref = Unsynchronized.ref []
1.204 - Provers/order.ML: val visited : term list Unsynchronized.ref = Unsynchronized.ref []
1.205 - Provers/order.ML: val visited : int list Unsynchronized.ref = Unsynchronized.ref []
1.206 - Provers/order.ML: val pred = Unsynchronized.ref [];
1.207 - Provers/order.ML: val visited = Unsynchronized.ref [];
1.208 -
1.209 - Pure/library.ML: val setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
1.210 - Pure/library.ML: val random_seed = Unsynchronized.ref 1.0;
1.211 -@ Pure/System/isar.ML: val global_history = Unsynchronized.ref ([]: history);
1.212 -@ Pure/System/isar.ML: val global_state = Unsynchronized.ref Toplevel.toplevel;
1.213 - Pure/System/isar.ML: val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
1.214 - Pure/System/session.ML:val session = Unsynchronized.ref ([Context.PureN]: string list);
1.215 - Pure/System/session.ML:val session_finished = Unsynchronized.ref false;
1.216 - Pure/System/session.ML:val session_path = Unsynchronized.ref ([]: string list);
1.217 - Pure/System/session.ML:val remote_path = Unsynchronized.ref (NONE: Url.T option);
1.218 - Pure/System/isabelle_process.ML:val tracing_messages = Unsynchronized.ref 100;
1.219 - Pure/ML-Systems/compiler_polyml.ML: val line = Unsynchronized.ref start_line;
1.220 - Pure/ML-Systems/compiler_polyml.ML: val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
1.221 - Pure/ML-Systems/compiler_polyml.ML: val out_buffer = Unsynchronized.ref ([]: string list);
1.222 - Pure/ML-Systems/polyml.ML: val depth = Unsynchronized.ref 10;
1.223 - Pure/Syntax/printer.ML:val show_brackets_default = Unsynchronized.ref false;
1.224 - Pure/Syntax/printer.ML:val show_types_default = Unsynchronized.ref false;
1.225 - Pure/Syntax/printer.ML:val show_sorts_default = Unsynchronized.ref false;
1.226 - Pure/Syntax/printer.ML:val show_markup_default = Unsynchronized.ref false;
1.227 - Pure/Syntax/printer.ML:val show_question_marks_default = Unsynchronized.ref true;
1.228 - Pure/Syntax/syntax_trans.ML:val eta_contract_default = Unsynchronized.ref true;
1.229 - Pure/Syntax/syntax_phases.ML: val reports = Unsynchronized.ref ([]: Position.report list);
1.230 - Pure/Syntax/syntax_phases.ML: val reports = Unsynchronized.ref reports0;
1.231 - Pure/Syntax/ast.ML: val passes = Unsynchronized.ref 0;
1.232 - Pure/Syntax/ast.ML: val failed_matches = Unsynchronized.ref 0;
1.233 - Pure/Syntax/ast.ML: val changes = Unsynchronized.ref 0;
1.234 - Pure/Proof/reconstruct.ML:val quiet_mode = Unsynchronized.ref true;
1.235 - Pure/Proof/extraction.ML: val cache = Unsynchronized.ref ([] : (term * term) list);
1.236 - Pure/Isar/runtime.ML:val debug = Unsynchronized.ref false;
1.237 - Pure/Isar/token.ML:fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
1.238 - Pure/Isar/token.ML:fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
1.239 - Pure/Isar/toplevel.ML:val quiet = Unsynchronized.ref false;
1.240 - Pure/Isar/toplevel.ML:val interact = Unsynchronized.ref false;
1.241 - Pure/Isar/toplevel.ML:val timing = Unsynchronized.ref false;
1.242 - Pure/Isar/toplevel.ML:val profiling = Unsynchronized.ref 0;
1.243 - Pure/Isar/toplevel.ML:val skip_proofs = Unsynchronized.ref false;
1.244 -@ Pure/Isar/toplevel.ML: val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
1.245 - Pure/Isar/proof.ML: val testing = Unsynchronized.ref false;
1.246 - Pure/Isar/proof.ML: val rule = Unsynchronized.ref (NONE: thm option);
1.247 - Pure/Isar/outer_syntax.ML:val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
1.248 - Pure/Isar/keyword.ML: Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty));
1.249 -
1.250 ---- ProofGeneral L"AUFT AUS ...
1.251 - Pure/ProofGeneral/proof_general_emacs.ML:val initialized = Unsynchronized.ref false;
1.252 - Pure/ProofGeneral/proof_general_pgip.ML:val pgmlsymbols_flag = Unsynchronized.ref true;
1.253 - Pure/ProofGeneral/proof_general_pgip.ML:val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
1.254 - Pure/ProofGeneral/proof_general_pgip.ML:val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref;
1.255 - Pure/ProofGeneral/proof_general_pgip.ML: val pgip_id = Unsynchronized.ref ""
1.256 - Pure/ProofGeneral/proof_general_pgip.ML: val pgip_seq = Unsynchronized.ref 0
1.257 - Pure/ProofGeneral/proof_general_pgip.ML:val output_xml_fn = Unsynchronized.ref Output.physical_writeln
1.258 - Pure/ProofGeneral/proof_general_pgip.ML:val show_theorem_dependencies = Unsynchronized.ref false;
1.259 - Pure/ProofGeneral/proof_general_pgip.ML:val preferences = Unsynchronized.ref Preferences.pure_preferences;
1.260 - Pure/ProofGeneral/proof_general_pgip.ML:val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
1.261 - Pure/ProofGeneral/proof_general_pgip.ML:val initialized = Unsynchronized.ref false;
1.262 - Pure/ProofGeneral/proof_general_pgip.ML: val pgip_output_channel = Unsynchronized.ref Output.physical_writeln
1.263 - Pure/ProofGeneral/preferences.ML: 'a Unsynchronized.ref -> string -> string -> preference
1.264 - Pure/ProofGeneral/preferences.ML: val string_pref: string Unsynchronized.ref -> string -> string -> preference
1.265 - Pure/ProofGeneral/preferences.ML: val real_pref: real Unsynchronized.ref -> string -> string -> preference
1.266 - Pure/ProofGeneral/preferences.ML: val int_pref: int Unsynchronized.ref -> string -> string -> preference
1.267 - Pure/ProofGeneral/preferences.ML: val nat_pref: int Unsynchronized.ref -> string -> string -> preference
1.268 - Pure/ProofGeneral/preferences.ML: val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
1.269 -
1.270 - Pure/term_sharing.ML: val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table);
1.271 - Pure/term_sharing.ML: val terms = Unsynchronized.ref (Syntax_Termtab.empty: unit Syntax_Termtab.table);
1.272 - Pure/term_subst.ML: let val maxidx = Unsynchronized.ref i
1.273 - Pure/term_subst.ML: let val maxidx = Unsynchronized.ref i
1.274 - Pure/term_subst.ML: | instantiateT_same instT ty = instT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty;
1.275 - Pure/term_subst.ML: | instantiate_same insts tm = inst_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm;
1.276 - Pure/pattern.ML:val trace_unify_fail = Unsynchronized.ref false;
1.277 - Pure/unify.ML: (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
1.278 - Pure/unify.ML: if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
1.279 - Pure/context.ML:val timing = Unsynchronized.ref false;
1.280 - Pure/context.ML: {self: theory Unsynchronized.ref option, (*dynamic self reference -- follows theory changes*)
1.281 - Pure/context.ML: SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
1.282 - Pure/context.ML: val r = Unsynchronized.ref thy;
1.283 - Pure/context.ML:fun deref (Theory_Ref (Unsynchronized.ref thy)) = thy;
1.284 -@ Pure/Concurrent/synchronized_sequential.ML:fun var _ x = Var (Unsynchronized.ref x);
1.285 - Pure/Concurrent/time_limit.ML: val timeout = Unsynchronized.ref false;
1.286 - Pure/Concurrent/synchronized.ML: var = Unsynchronized.ref x};
1.287 - Pure/Concurrent/future.ML:val queue = Unsynchronized.ref Task_Queue.empty;
1.288 - Pure/Concurrent/future.ML:val next = Unsynchronized.ref 0;
1.289 - Pure/Concurrent/future.ML:val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
1.290 - Pure/Concurrent/future.ML:val canceled = Unsynchronized.ref ([]: group list);
1.291 - Pure/Concurrent/future.ML:val do_shutdown = Unsynchronized.ref false;
1.292 - Pure/Concurrent/future.ML:val max_workers = Unsynchronized.ref 0;
1.293 - Pure/Concurrent/future.ML:val max_active = Unsynchronized.ref 0;
1.294 - Pure/Concurrent/future.ML:val worker_trend = Unsynchronized.ref 0;
1.295 - Pure/Concurrent/future.ML:val status_ticks = Unsynchronized.ref 0;
1.296 - Pure/Concurrent/future.ML:val last_round = Unsynchronized.ref Time.zeroTime;
1.297 -@ Pure/Concurrent/future.ML:val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list);
1.298 - Pure/Concurrent/future.ML:val ML_statistics = Unsynchronized.ref false;
1.299 - Pure/Concurrent/future.ML:val forked_proofs = Unsynchronized.ref 0;
1.300 -@ Pure/Concurrent/future.ML: Unsynchronized.ref Working));
1.301 - Pure/Concurrent/lazy_sequential.ML:fun lazy e = Lazy (Unsynchronized.ref (Expr e));
1.302 - Pure/Concurrent/lazy_sequential.ML:fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
1.303 - Pure/General/secure.ML:val secure = Unsynchronized.ref false;
1.304 - Pure/General/pretty.ML:val margin_default = Unsynchronized.ref 76; (*right margin, or page width*)
1.305 - Pure/General/name_space.ML:val names_long_default = Unsynchronized.ref false;
1.306 - Pure/General/name_space.ML:val names_short_default = Unsynchronized.ref false;
1.307 - Pure/General/name_space.ML:val names_unique_default = Unsynchronized.ref true;
1.308 - Pure/General/position.ML: val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
1.309 - Pure/General/print_mode.ML: val print_mode: string list Unsynchronized.ref (*global template*)
1.310 - Pure/General/print_mode.ML:val print_mode = Unsynchronized.ref ([]: string list);
1.311 - Pure/General/output.ML: val writeln_fn = Unsynchronized.ref physical_writeln;
1.312 - Pure/General/output.ML: val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
1.313 - Pure/General/output.ML: val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
1.314 - Pure/General/output.ML: val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
1.315 - Pure/General/output.ML: val error_fn = Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
1.316 - Pure/General/output.ML: val prompt_fn = Unsynchronized.ref physical_stdout;
1.317 - Pure/General/output.ML: val status_fn = Unsynchronized.ref (fn _: output => ());
1.318 - Pure/General/output.ML: val report_fn = Unsynchronized.ref (fn _: output => ());
1.319 - Pure/General/output.ML: val result_fn = Unsynchronized.ref (fn _: serial * output => ());
1.320 - Pure/General/output.ML: val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
1.321 -@ Pure/General/output.ML: Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
1.322 - Pure/Tools/find_theorems.ML:val tac_limit = Unsynchronized.ref 5;
1.323 - Pure/Tools/find_theorems.ML:val limit = Unsynchronized.ref 40;
1.324 - Pure/raw_simplifier.ML:val simp_trace_depth_limit_default = Unsynchronized.ref 1;
1.325 - Pure/raw_simplifier.ML: if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context));
1.326 - Pure/raw_simplifier.ML:val simp_trace_default = Unsynchronized.ref false;
1.327 - Pure/raw_simplifier.ML: make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
1.328 - Pure/raw_simplifier.ML:val debug_bounds = Unsynchronized.ref false;
1.329 - Pure/ROOT.ML:val quick_and_dirty = Unsynchronized.ref false;
1.330 - Pure/goal_display.ML:val goals_limit_default = Unsynchronized.ref 10;
1.331 - Pure/goal_display.ML:val show_main_goal_default = Unsynchronized.ref false;
1.332 - Pure/goal_display.ML:val show_consts_default = Unsynchronized.ref false;
1.333 - Pure/ML/ml_compiler_polyml.ML: Unsynchronized.ref (toks |> map
1.334 - Pure/ML/ml_compiler_polyml.ML: val writeln_buffer = Unsynchronized.ref Buffer.empty;
1.335 - Pure/ML/ml_compiler_polyml.ML: val warnings = Unsynchronized.ref ([]: string list);
1.336 - Pure/ML/ml_compiler_polyml.ML: val error_buffer = Unsynchronized.ref Buffer.empty;
1.337 -@ Pure/goal.ML:val parallel_proofs = Unsynchronized.ref 1;
1.338 - Pure/goal.ML:val parallel_proofs_threshold = Unsynchronized.ref 50;
1.339 - Pure/tactical.ML: val tracify: bool Unsynchronized.ref -> tactic -> tactic
1.340 - Pure/tactical.ML:val trace_REPEAT= Unsynchronized.ref false
1.341 - Pure/tactical.ML:and suppress_tracing = Unsynchronized.ref false;
1.342 - Pure/type.ML: val tyvar_count = Unsynchronized.ref maxidx;
1.343 -@ Pure/PIDE/document.ML: (no_id, Future.new_group NONE, Unsynchronized.ref false));
1.344 -@ Pure/PIDE/document.ML: val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
1.345 - Pure/PIDE/document.ML:val timing = Unsynchronized.ref false;
1.346 - Pure/search.ML:val trace_DEPTH_FIRST = Unsynchronized.ref false;
1.347 - Pure/search.ML: let val countr = Unsynchronized.ref 0
1.348 - Pure/search.ML:val trace_DEEPEN = Unsynchronized.ref false;
1.349 - Pure/search.ML:val trace_BEST_FIRST = Unsynchronized.ref false;
1.350 - Pure/search.ML:val trace_ASTAR = Unsynchronized.ref false;
1.351 - Pure/Thy/thy_output.ML:val display_default = Unsynchronized.ref false;
1.352 - Pure/Thy/thy_output.ML:val quotes_default = Unsynchronized.ref false;
1.353 - Pure/Thy/thy_output.ML:val indent_default = Unsynchronized.ref 0;
1.354 - Pure/Thy/thy_output.ML:val source_default = Unsynchronized.ref false;
1.355 - Pure/Thy/thy_output.ML:val break_default = Unsynchronized.ref false;
1.356 - Pure/Thy/thy_output.ML:val modes = Unsynchronized.ref ([]: string list);
1.357 - Pure/Thy/thy_load.ML: val master_path = Unsynchronized.ref Path.current;
1.358 - Pure/Thy/present.ML:val browser_info = Unsynchronized.ref empty_browser_info;
1.359 - Pure/Thy/present.ML:val suppress_tex_source = Unsynchronized.ref false;
1.360 - Pure/Thy/present.ML:val session_info = Unsynchronized.ref (NONE: session_info option);
1.361 - Pure/Thy/thy_info.ML: Unsynchronized.ref (String_Graph.empty: (deps option * theory option) String_Graph.T);
1.362 -@ Pure/proofterm.ML:val proofs = Unsynchronized.ref 2;
1.363 -
1.364 ---- Tools concerns external provers, Isac shall use in the future --- thus observe conflicts
1.365 - Sequents/prover.ML:val trace = Unsynchronized.ref false;
1.366 - Tools/Code/code_runtime.ML:val trace = Unsynchronized.ref false;
1.367 - Tools/WWW_Find/scgi_server.ML:val max_threads = Unsynchronized.ref 5;
1.368 - Tools/WWW_Find/scgi_server.ML:val servers = Unsynchronized.ref (Symtab.empty : (Mime.t option * handler) Symtab.table);
1.369 - Tools/WWW_Find/scgi_server.ML: val threads = Unsynchronized.ref ([] : Thread.thread list);
1.370 - Tools/misc_legacy.ML:val gensym_seed = Unsynchronized.ref (0: int);
1.371 - Tools/Metis/metis.ML:local val rand = (*Unsynchronized.*)Unsynchronized.ref 0w1
1.372 - Tools/Metis/metis.ML:val withRef : 'r Unsynchronized.ref * 'r -> ('a -> 'b) -> 'a -> 'b
1.373 - Tools/Metis/metis.ML: val tracePrint = Unsynchronized.ref tracePrintFn;
1.374 - Tools/Metis/metis.ML: val generator = Unsynchronized.ref 0
1.375 - Tools/Metis/metis.ML:fun quickly v = Metis_Lazy (Unsynchronized.ref (Value v));
1.376 - Tools/Metis/metis.ML:fun delay f = Metis_Lazy (Unsynchronized.ref (Thunk f));
1.377 - Tools/Metis/metis.ML: val cache = Unsynchronized.ref (Metis_Map.new cmp)
1.378 - Tools/Metis/metis.ML:val lineLength = Unsynchronized.ref initialLineLength;
1.379 - Tools/Metis/metis.ML: val lastLine = Unsynchronized.ref (~1,"","","")
1.380 - Tools/Metis/metis.ML: val Unsynchronized.ref (n,_,l2,l3) = lastLine
1.381 - Tools/Metis/metis.ML: val Unsynchronized.ref (n,l1,l2,l3) = lastLine
1.382 - Tools/Metis/metis.ML: (Unsynchronized.ref o Metis_Print.Infixes)
1.383 - Tools/Metis/metis.ML:val negation : string Unsynchronized.ref = Unsynchronized.ref "~";
1.384 - Tools/Metis/metis.ML:val binders : string list Unsynchronized.ref = Unsynchronized.ref ["\\","!","?","?!"];
1.385 - Tools/Metis/metis.ML:val brackets : (string * string) list Unsynchronized.ref = Unsynchronized.ref [("[","]"),("{","}")];
1.386 - Tools/Metis/metis.ML: val Unsynchronized.ref s = Metis_Term.negation
1.387 - Tools/Metis/metis.ML: val counter : int Metis_StringMap.map Unsynchronized.ref = Unsynchronized.ref (Metis_StringMap.new ());
1.388 - Tools/Metis/metis.ML: val Unsynchronized.ref m = counter
1.389 - Tools/Metis/metis.ML: val counter : int Unsynchronized.ref = Unsynchronized.ref 0;
1.390 - Tools/Metis/metis.ML: val Unsynchronized.ref i = counter
1.391 - Tools/Metis/metis.ML: tableMap = Unsynchronized.ref (Metis_NameArityMap.new ())};
1.392 - Tools/Metis/metis.ML: val Unsynchronized.ref m = tm
1.393 - Tools/Metis/metis.ML: val r = Unsynchronized.ref 0
1.394 - Tools/Metis/metis.ML: val Unsynchronized.ref n = r
1.395 - Tools/Metis/metis.ML:val showId = Unsynchronized.ref false;
1.396 -
1.397 - Tools/coherent.ML:val verbose = Unsynchronized.ref false;
1.398 - Tools/coherent.ML:val show_facts = Unsynchronized.ref false;
1.399 - Tools/nbe.ML:val trace = Unsynchronized.ref false;
1.400 - Tools/quickcheck.ML: val add_timing : (string * int) -> result Unsynchronized.ref -> unit
1.401 - Tools/quickcheck.ML: val add_response : string list -> term list -> (bool * term list) option -> result Unsynchronized.ref -> unit
1.402 - Tools/quickcheck.ML: val add_report : int -> report option -> result Unsynchronized.ref -> unit
1.403 - Tools/quickcheck.ML:val auto = Unsynchronized.ref false;
1.404 - Tools/solve_direct.ML:val auto = Unsynchronized.ref false;
1.405 - Tools/solve_direct.ML:val max_solutions = Unsynchronized.ref 5;
1.406 - Tools/try.ML:val auto_time_limit = Unsynchronized.ref 4.0
1.407 -
1.408 - Tools/isac/Frontend/states.sml:val states = Unsynchronized.ref ([]:(iterID * (calcID * state) list) list);
1.409 -!! Tools/isac/calcelems.sml:val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
1.410 -!! Tools/isac/calcelems.sml:val isabthys = Unsynchronized.ref ([] : theory list);
1.411 -!! Tools/isac/calcelems.sml:val knowthys = Unsynchronized.ref ([] : theory list);
1.412 -!! Tools/isac/calcelems.sml:val progthys = Unsynchronized.ref ([] : theory list);
1.413 -!! Tools/isac/calcelems.sml:val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
1.414 -!! Tools/isac/calcelems.sml:val calclist'= Unsynchronized.ref ([]: calc list);
1.415 -!! Tools/isac/calcelems.sml:val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
1.416 -!! Tools/isac/calcelems.sml:val isab_thm_thy = Unsynchronized.ref ([] : (thmDeriv * term) list);
1.417 -!! Tools/isac/calcelems.sml:val isabthys = Unsynchronized.ref ([] : theory list);
1.418 -!! Tools/isac/calcelems.sml:val first_ProgLang_thy = Unsynchronized.ref (@{theory Pure});
1.419 -!! Tools/isac/calcelems.sml:val first_Knowledge_thy = Unsynchronized.ref (@{theory Pure});
1.420 - Tools/isac/calcelems.sml:val trace_rewrite = Unsynchronized.ref false;
1.421 - Tools/isac/calcelems.sml:val depth = Unsynchronized.ref 99999;
1.422 - Tools/isac/calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999;
1.423 - Tools/isac/calcelems.sml:val lim_deriv = Unsynchronized.ref 100;
1.424 - Tools/isac/calcelems.sml:val check_guhs_unique = Unsynchronized.ref true;
1.425 -!? Tools/isac/ProgLang/Script.thy:val tacs = Unsynchronized.ref (distinct (remove op = ""
1.426 -!? Tools/isac/ProgLang/Script.thy:val screxpr = Unsynchronized.ref (distinct (remove op = ""
1.427 -!? Tools/isac/ProgLang/Script.thy:val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *)
1.428 -!? Tools/isac/ProgLang/Script.thy:val scrfuns = Unsynchronized.ref ([]: string list);
1.429 -!? Tools/isac/ProgLang/Script.thy:val listexpr = Unsynchronized.ref (union op = (!listfuns) (!scrfuns));
1.430 -!? Tools/isac/ProgLang/Script.thy:val notsimp = Unsynchronized.ref
1.431 -!? Tools/isac/ProgLang/Script.thy:val negotiable = Unsynchronized.ref ((!tacs (*@ !subpbls*)));
1.432 - Tools/isac/Knowledge/GCD_Poly_ML.thy: val trace_div = Unsynchronized.ref true;
1.433 - Tools/isac/Knowledge/GCD_Poly_ML.thy: val trace_div_invariant = Unsynchronized.ref false; (*.. true expects !trace_div = false *)
1.434 - Tools/isac/Knowledge/GCD_Poly_ML.thy: val trace_Euclid = Unsynchronized.ref true;
1.435 -!! Tools/isac/Interpret/inform.sml:val castab = Unsynchronized.ref ([]: castab);
1.436 - Tools/isac/Interpret/script.sml:val trace_script = Unsynchronized.ref false;
1.437 -!! Tools/isac/Interpret/ptyps.sml:val pbltypes = Unsynchronized.ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)
1.438 -!! Tools/isac/Interpret/ptyps.sml:val ptyps = Unsynchronized.ref ([e_Ptyp]:ptyps);
1.439 -!! Tools/isac/Interpret/ptyps.sml:val mets = Unsynchronized.ref ([e_Mets]:mets);
1.440 - Tools/isac/Interpret/ctree.sml:> val pt = Unsynchronized.ref EmptyPtree;
1.441 -!? Tools/isac/Interpret/ctree.sml: val pt = Unsynchronized.ref Empty;
1.442 -
1.443 - ZF/ind_syntax.ML:val trace = Unsynchronized.ref false;
1.444 - ZF/Datatype_ZF.thy: val trace = Unsynchronized.ref false;