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