1 neuper@neuper:/usr/local/isabisac/src$ grep -r "Unsynchronized.ref " * |
|
2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
3 relevance for Isac's parallel math-engine: # low .. ##### high |
|
4 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
5 legend: |
|
6 --- comments |
|
7 !! to be replaced by Theory_Data |
|
8 !? to be replaced by other means |
|
9 @ first quick marks for possible relevance |
|
10 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
11 |
|
12 Doc/IsarImplementation/ML.thy: @{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\ |
|
13 Doc/IsarImplementation/ML.thy: @{index_ML_op ":=": "'a Unsynchronized.ref * 'a -> unit"} \\ |
|
14 FOLP/simp.ML:val tracing = Unsynchronized.ref false; |
|
15 HOL/HOLCF/Tools/Domain/domain_induction.ML:val quiet_mode = Unsynchronized.ref false |
|
16 |
|
17 --- Isac is a level deeper than HOL, at level Pure ... |
|
18 HOL/HOLCF/Tools/Domain/domain_induction.ML:val trace_domain = Unsynchronized.ref false |
|
19 HOL/Matrix_LP/Cplex_tools.ML:val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT; |
|
20 HOL/Matrix_LP/Cplex_tools.ML: val ignore_NL = Unsynchronized.ref true |
|
21 HOL/Matrix_LP/Cplex_tools.ML: val rest = Unsynchronized.ref [] |
|
22 HOL/Matrix_LP/Cplex_tools.ML: val linebuf = Unsynchronized.ref "" |
|
23 HOL/Matrix_LP/Cplex_tools.ML: val rest = Unsynchronized.ref [] |
|
24 HOL/Matrix_LP/Cplex_tools.ML: val rest = Unsynchronized.ref [] |
|
25 HOL/Matrix_LP/FloatSparseMatrixBuilder.ML: val ytable = Unsynchronized.ref Inttab.empty |
|
26 HOL/Matrix_LP/FloatSparseMatrixBuilder.ML: val count = Unsynchronized.ref 0; |
|
27 HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML:val max_reductions = Unsynchronized.ref (NONE : int option) |
|
28 HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML: val s = Unsynchronized.ref (Continue p) |
|
29 HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML: val counter = Unsynchronized.ref 0 |
|
30 HOL/Matrix_LP/Compute_Oracle/compute.ML: (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) |
|
31 HOL/Matrix_LP/Compute_Oracle/compute.ML:fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy |
|
32 HOL/Matrix_LP/Compute_Oracle/compute.ML:fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps |
|
33 HOL/Matrix_LP/Compute_Oracle/compute.ML:fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable) |
|
34 HOL/Matrix_LP/Compute_Oracle/compute.ML:fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable |
|
35 HOL/Matrix_LP/Compute_Oracle/compute.ML:fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp |
|
36 HOL/Matrix_LP/Compute_Oracle/compute.ML:fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog |
|
37 HOL/Matrix_LP/Compute_Oracle/compute.ML:fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding |
|
38 HOL/Matrix_LP/Compute_Oracle/compute.ML:fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,_,p2,p3,p4,p5,p6)))) encoding' = |
|
39 HOL/Matrix_LP/Compute_Oracle/compute.ML:fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n |
|
40 HOL/Matrix_LP/Compute_Oracle/compute.ML:fun set_naming (Computer (r as Unsynchronized.ref (SOME (p1,p2,p3,p4,p5,p6,_)))) naming'= |
|
41 HOL/Matrix_LP/Compute_Oracle/compute.ML: Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms))) |
|
42 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 |
|
43 HOL/Matrix_LP/Compute_Oracle/am_sml.ML: val dump_output : (string option) Unsynchronized.ref |
|
44 HOL/Matrix_LP/Compute_Oracle/am_sml.ML:val dump_output = Unsynchronized.ref (NONE: string option) |
|
45 HOL/Matrix_LP/Compute_Oracle/am_sml.ML:val saved_result = Unsynchronized.ref (NONE:(string*term)option) |
|
46 HOL/Matrix_LP/Compute_Oracle/am_sml.ML:val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) |
|
47 HOL/Matrix_LP/Compute_Oracle/am_sml.ML: val buffer = Unsynchronized.ref "" |
|
48 HOL/Matrix_LP/Compute_Oracle/am_sml.ML:val guid_counter = Unsynchronized.ref 0 |
|
49 HOL/Matrix_LP/Compute_Oracle/linker.ML: PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref * |
|
50 HOL/Matrix_LP/Compute_Oracle/linker.ML: pattern list Unsynchronized.ref |
|
51 HOL/Matrix_LP/Compute_Oracle/linker.ML: val changed = Unsynchronized.ref false |
|
52 HOL/Matrix_LP/Compute_Oracle/linker.ML: val counter = Unsynchronized.ref 0 |
|
53 HOL/Matrix_LP/Compute_Oracle/linker.ML: val tab = Unsynchronized.ref (CThmtab.empty : unit CThmtab.table) |
|
54 HOL/Matrix_LP/Compute_Oracle/linker.ML: val thstab = Unsynchronized.ref (Inttab.empty : thm Inttab.table) |
|
55 HOL/Matrix_LP/Compute_Oracle/linker.ML: PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats) |
|
56 HOL/Matrix_LP/Compute_Oracle/am_compiler.ML:val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) |
|
57 HOL/Matrix_LP/Compute_Oracle/am_compiler.ML: val buffer = Unsynchronized.ref "" |
|
58 HOL/Matrix_LP/Compute_Oracle/am_compiler.ML: " val s = Unsynchronized.ref (Continue p)", |
|
59 HOL/Matrix_LP/Compute_Oracle/am_ghc.ML: val buffer = Unsynchronized.ref "" |
|
60 HOL/Matrix_LP/Compute_Oracle/am_ghc.ML:val guid_counter = Unsynchronized.ref 0 |
|
61 HOL/Matrix_LP/Compute_Oracle/report.ML: val report_depth = Unsynchronized.ref 0 |
|
62 HOL/Random.thy:val seed = Unsynchronized.ref |
|
63 HOL/Mutabelle/mutabelle_extra.ML:val random_seed = Unsynchronized.ref 1.0; |
|
64 HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML:val data = Unsynchronized.ref ([] : (int * data) list) |
|
65 HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML:val num_sledgehammer_calls = Unsynchronized.ref 0 |
|
66 HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML: val reconstructor = Unsynchronized.ref "" |
|
67 HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML: Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) |
|
68 HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val proof_table = Unsynchronized.ref (Prooftab.empty: string list list Prooftab.table) |
|
69 HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_successes = Unsynchronized.ref ([] : (int * int) list) |
|
70 HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_failures = Unsynchronized.ref ([] : (int * int) list) |
|
71 HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_found_proofs = Unsynchronized.ref ([] : (int * int) list) |
|
72 HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_lost_proofs = Unsynchronized.ref ([] : (int * int) list) |
|
73 HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_found_facts = Unsynchronized.ref ([] : (int * int) list) |
|
74 HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML:val num_lost_facts = Unsynchronized.ref ([] : (int * int) list) |
|
75 HOL/Statespace/DistinctTreeProver.thy:val da = Unsynchronized.ref refl; |
|
76 HOL/Tools/try0.ML:val auto = Unsynchronized.ref false |
|
77 HOL/Tools/Function/scnp_solve.ML:val solver = Unsynchronized.ref "auto"; |
|
78 HOL/Tools/Function/function_core.ML:val trace = Unsynchronized.ref false |
|
79 HOL/Tools/Function/function_common.ML:val profile = Unsynchronized.ref false; |
|
80 HOL/Tools/sat_funcs.ML: val trace_sat: bool Unsynchronized.ref (* input: print trace messages *) |
|
81 HOL/Tools/sat_funcs.ML: val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *) |
|
82 HOL/Tools/sat_funcs.ML: val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *) |
|
83 HOL/Tools/sat_funcs.ML:val trace_sat = Unsynchronized.ref false; |
|
84 HOL/Tools/sat_funcs.ML:val solver = Unsynchronized.ref "zchaff_with_proofs"; |
|
85 HOL/Tools/sat_funcs.ML:val counter = Unsynchronized.ref 0; |
|
86 HOL/Tools/Sledgehammer/sledgehammer_provers.ML:val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x) |
|
87 HOL/Tools/Sledgehammer/sledgehammer_isar.ML:val auto = Unsynchronized.ref false |
|
88 HOL/Tools/Sledgehammer/sledgehammer_isar.ML:val provers = Unsynchronized.ref "" |
|
89 HOL/Tools/Sledgehammer/sledgehammer_isar.ML:val timeout = Unsynchronized.ref 30 |
|
90 HOL/Tools/Nitpick/nitpick.ML: val state_ref = Unsynchronized.ref state |
|
91 HOL/Tools/Nitpick/nitpick.ML: val simp_table = Unsynchronized.ref (const_simp_table ctxt subst) |
|
92 HOL/Tools/Nitpick/nitpick.ML: ersatz_table = ersatz_table, skolems = Unsynchronized.ref [], |
|
93 HOL/Tools/Nitpick/nitpick.ML: special_funs = Unsynchronized.ref [], |
|
94 HOL/Tools/Nitpick/nitpick.ML: unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], |
|
95 HOL/Tools/Nitpick/nitpick.ML: constr_cache = Unsynchronized.ref []} |
|
96 HOL/Tools/Nitpick/nitpick.ML: val too_big_scopes = Unsynchronized.ref [] |
|
97 HOL/Tools/Nitpick/nitpick.ML: val scopes = Unsynchronized.ref [] |
|
98 HOL/Tools/Nitpick/nitpick.ML: val generated_scopes = Unsynchronized.ref [] |
|
99 HOL/Tools/Nitpick/nitpick.ML: val generated_problems = Unsynchronized.ref ([] : rich_problem list) |
|
100 HOL/Tools/Nitpick/nitpick.ML: val checked_problems = Unsynchronized.ref (SOME []) |
|
101 HOL/Tools/Nitpick/nitpick.ML: val met_potential = Unsynchronized.ref 0 |
|
102 HOL/Tools/Nitpick/nitpick_hol.ML: val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit |
|
103 HOL/Tools/Nitpick/nitpick_mono.ML:val trace = Unsynchronized.ref false |
|
104 HOL/Tools/Nitpick/nitpick_mono.ML: max_fresh = Unsynchronized.ref 0, datatype_mcache = Unsynchronized.ref [], |
|
105 HOL/Tools/Nitpick/nitpick_mono.ML: constr_mcache = Unsynchronized.ref []} : mdata) |
|
106 HOL/Tools/Nitpick/kodkod.ML:val created_temp_dir = Unsynchronized.ref false |
|
107 HOL/Tools/Nitpick/kodkod.ML: val in_buf = Unsynchronized.ref Buffer.empty |
|
108 HOL/Tools/Nitpick/nitpick_isar.ML:val auto = Unsynchronized.ref false |
|
109 HOL/Tools/Nitpick/nitpick_model.ML: val pool = Unsynchronized.ref [] |
|
110 HOL/Tools/Nitpick/nitpick_model.ML: val pool = Unsynchronized.ref [] |
|
111 HOL/Tools/Meson/meson.ML: let val ctxt0r = Unsynchronized.ref ctxt0 (* FIXME ??? *) |
|
112 HOL/Tools/Quickcheck/random_generators.ML: val state = Unsynchronized.ref (seed'', [], fn () => Abs ("x", T1, t2 ())); |
|
113 HOL/Tools/Quickcheck/narrowing_generators.ML: val current_size = Unsynchronized.ref 0 |
|
114 HOL/Tools/Quickcheck/narrowing_generators.ML: val current_result = Unsynchronized.ref Quickcheck.empty_result |
|
115 HOL/Tools/Quickcheck/quickcheck_common.ML: val current_size = Unsynchronized.ref 0 |
|
116 HOL/Tools/Quickcheck/quickcheck_common.ML: val current_result = Unsynchronized.ref Quickcheck.empty_result |
|
117 HOL/Tools/Quickcheck/quickcheck_common.ML: val current_result = Unsynchronized.ref Quickcheck.empty_result |
|
118 HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML:val nrandom = Unsynchronized.ref 3; |
|
119 HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML:val debug = Unsynchronized.ref false; |
|
120 HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML:val no_higher_order_predicate = Unsynchronized.ref ([] : string list); |
|
121 HOL/Tools/Predicate_Compile/predicate_compile.ML:val present_graph = Unsynchronized.ref false |
|
122 HOL/Tools/Predicate_Compile/predicate_compile.ML:val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref |
|
123 HOL/Tools/Predicate_Compile/code_prolog.ML:val trace = Unsynchronized.ref false |
|
124 HOL/Tools/sat_solver.ML: val solvers = Unsynchronized.ref ([] : (string * solver) list); |
|
125 HOL/Tools/sat_solver.ML: val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1) |
|
126 HOL/Tools/sat_solver.ML: val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) |
|
127 HOL/Tools/sat_solver.ML: val empty_id = Unsynchronized.ref ~1 |
|
128 HOL/Tools/sat_solver.ML: val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table) |
|
129 HOL/Tools/sat_solver.ML: val next_id = Unsynchronized.ref (number_of_clauses - 1) |
|
130 HOL/Tools/sat_solver.ML: val clause_offset = Unsynchronized.ref ~1 |
|
131 HOL/Tools/sat_solver.ML: val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) |
|
132 HOL/Tools/sat_solver.ML: val empty_id = Unsynchronized.ref ~1 |
|
133 HOL/Tools/prop_logic.ML: val new = Unsynchronized.ref (maxidx fm' + 1) |
|
134 HOL/Tools/prop_logic.ML: val next_idx_is_valid = Unsynchronized.ref false |
|
135 HOL/Tools/prop_logic.ML: val next_idx = Unsynchronized.ref 0 |
|
136 HOL/Tools/TFL/rules.ML:val tracing = Unsynchronized.ref false; |
|
137 HOL/Tools/TFL/rules.ML: val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref |
|
138 HOL/Tools/TFL/tfl.ML:val trace = Unsynchronized.ref false; |
|
139 HOL/Tools/TFL/tfl.ML: let val slist = Unsynchronized.ref names |
|
140 HOL/Tools/TFL/tfl.ML: val vname = Unsynchronized.ref "u" |
|
141 HOL/Tools/cnf_funcs.ML: val var_id = Unsynchronized.ref 0 (* properly initialized below *) |
|
142 HOL/TPTP/TPTP_Parser/tptp_parser.ML: val currentPos = Unsynchronized.ref 0 |
|
143 HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML: datatype 'a str = EVAL of 'a * 'a str Unsynchronized.ref | UNEVAL of (unit->'a) |
|
144 HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML:val col = Unsynchronized.ref 0; |
|
145 HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML:val linep = Unsynchronized.ref 1; (* Line pointer *) |
|
146 HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML:val eolpos = Unsynchronized.ref 0; |
|
147 HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yyb = Unsynchronized.ref "\n" (* buffer *) |
|
148 HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yybl = Unsynchronized.ref 1 (*buffer length *) |
|
149 HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yybufpos = Unsynchronized.ref 1 (* location of next character to use *) |
|
150 HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yygone = Unsynchronized.ref yygone0 (* position in file of beginning of buffer *) |
|
151 HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yydone = Unsynchronized.ref false (* eof found yet? *) |
|
152 HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML: val yybegin = Unsynchronized.ref 1 (*Current 'start state' for lexer *) |
|
153 HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML:val s = Unsynchronized.ref "" and index = Unsynchronized.ref 0 |
|
154 HOL/Decision_Procs/cooper_tac.ML:val trace = Unsynchronized.ref false; |
|
155 HOL/Decision_Procs/mir_tac.ML:val trace = Unsynchronized.ref false; |
|
156 HOL/Decision_Procs/ferrack_tac.ML:val trace = Unsynchronized.ref false; |
|
157 HOL/Nitpick_Examples/Mono_Nits.thy:val simp_table = Unsynchronized.ref (const_simp_table ctxt subst) |
|
158 HOL/Nitpick_Examples/Mono_Nits.thy: skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], |
|
159 HOL/Nitpick_Examples/Mono_Nits.thy: unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], |
|
160 HOL/Nitpick_Examples/Mono_Nits.thy: constr_cache = Unsynchronized.ref []} |
|
161 HOL/ex/SVC_Oracle.thy: val vname = Unsynchronized.ref "V_a" |
|
162 HOL/ex/SVC_Oracle.thy: val pairs = Unsynchronized.ref ([] : (term*term) list) |
|
163 HOL/ex/svc_funcs.ML: val trace = Unsynchronized.ref false; |
|
164 HOL/ex/svc_funcs.ML: val nat_vars = Unsynchronized.ref ([] : string list) |
|
165 |
|
166 --- Provers are an internal part of Isabelle, where Isac should not conflict with |
|
167 Provers/blast.ML: | Skolem of string * term option Unsynchronized.ref list |
|
168 Provers/blast.ML: | Skolem of string * term option Unsynchronized.ref list |
|
169 Provers/blast.ML: vars: term option Unsynchronized.ref list, (*variables occurring in branch*) |
|
170 Provers/blast.ML: trail: term option Unsynchronized.ref list Unsynchronized.ref, |
|
171 Provers/blast.ML: names = Unsynchronized.ref (Variable.names_of ctxt), |
|
172 Provers/blast.ML: fullTrace = Unsynchronized.ref [], |
|
173 Provers/blast.ML: trail = Unsynchronized.ref [], |
|
174 Provers/blast.ML: ntrail = Unsynchronized.ref 0, |
|
175 Provers/blast.ML: nclosed = Unsynchronized.ref 0, (*number of branches closed during the search*) |
|
176 Provers/blast.ML: ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*) |
|
177 Provers/blast.ML: NONE => let val t' = Var (Unsynchronized.ref NONE) |
|
178 Provers/blast.ML: | t aconv (Var (Unsynchronized.ref (SOME u))) = t aconv u |
|
179 Provers/blast.ML: | add_term_vars (Var (v as Unsynchronized.ref NONE), vars) = ins_var (v, vars) |
|
180 Provers/blast.ML: | add_term_vars (Var (Unsynchronized.ref (SOME u)), vars) = add_term_vars (u, vars) |
|
181 Provers/blast.ML: | add_vars_vars (Unsynchronized.ref (SOME u) :: vs, vars) = |
|
182 Provers/blast.ML: | (Var (Unsynchronized.ref NONE)) => t |
|
183 Provers/blast.ML: | (Var (Unsynchronized.ref (SOME u))) => norm u |
|
184 Provers/blast.ML: let val alistVar = Unsynchronized.ref [] |
|
185 Provers/blast.ML: and alistTVar = Unsynchronized.ref [] |
|
186 Provers/blast.ML: NONE => let val t' = Var (Unsynchronized.ref NONE) |
|
187 Provers/blast.ML: let val name = Unsynchronized.ref "a" |
|
188 Provers/blast.ML: val updated = Unsynchronized.ref [] |
|
189 Provers/blast.ML: | inst (Var(v as Unsynchronized.ref NONE)) = (updated := v :: (!updated); |
|
190 Provers/blast.ML: Const (c, _) $ Var (Unsynchronized.ref (SOME (Const ("*False*", _)))) => |
|
191 Provers/blast.ML: | showTerm d (Var (Unsynchronized.ref NONE)) = dummyVar2 |
|
192 Provers/blast.ML: val alistVar = Unsynchronized.ref [] |
|
193 Provers/blast.ML: and alistTVar = Unsynchronized.ref [] |
|
194 Provers/blast.ML: NONE => (alistVar := (ix, (Unsynchronized.ref NONE, bounds ts)) |
|
195 Provers/trancl.ML: val pred = Unsynchronized.ref []; |
|
196 Provers/trancl.ML: val visited = Unsynchronized.ref []; |
|
197 Provers/trancl.ML: val visited = Unsynchronized.ref []; |
|
198 Provers/quasi.ML: val pred = Unsynchronized.ref []; |
|
199 Provers/quasi.ML: val visited = Unsynchronized.ref []; |
|
200 Provers/order.ML: val finish : term list Unsynchronized.ref = Unsynchronized.ref [] |
|
201 Provers/order.ML: val visited : term list Unsynchronized.ref = Unsynchronized.ref [] |
|
202 Provers/order.ML: val visited : int list Unsynchronized.ref = Unsynchronized.ref [] |
|
203 Provers/order.ML: val pred = Unsynchronized.ref []; |
|
204 Provers/order.ML: val visited = Unsynchronized.ref []; |
|
205 |
|
206 Pure/library.ML: val setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c |
|
207 Pure/library.ML: val random_seed = Unsynchronized.ref 1.0; |
|
208 @ Pure/System/isar.ML: val global_history = Unsynchronized.ref ([]: history); |
|
209 @ Pure/System/isar.ML: val global_state = Unsynchronized.ref Toplevel.toplevel; |
|
210 Pure/System/isar.ML: val global_exn = Unsynchronized.ref (NONE: (exn * string) option); |
|
211 Pure/System/session.ML:val session = Unsynchronized.ref ([Context.PureN]: string list); |
|
212 Pure/System/session.ML:val session_finished = Unsynchronized.ref false; |
|
213 Pure/System/session.ML:val session_path = Unsynchronized.ref ([]: string list); |
|
214 Pure/System/session.ML:val remote_path = Unsynchronized.ref (NONE: Url.T option); |
|
215 Pure/System/isabelle_process.ML:val tracing_messages = Unsynchronized.ref 100; |
|
216 Pure/ML-Systems/compiler_polyml.ML: val line = Unsynchronized.ref start_line; |
|
217 Pure/ML-Systems/compiler_polyml.ML: val in_buffer = Unsynchronized.ref (String.explode (tune_source txt)); |
|
218 Pure/ML-Systems/compiler_polyml.ML: val out_buffer = Unsynchronized.ref ([]: string list); |
|
219 Pure/ML-Systems/polyml.ML: val depth = Unsynchronized.ref 10; |
|
220 Pure/Syntax/printer.ML:val show_brackets_default = Unsynchronized.ref false; |
|
221 Pure/Syntax/printer.ML:val show_types_default = Unsynchronized.ref false; |
|
222 Pure/Syntax/printer.ML:val show_sorts_default = Unsynchronized.ref false; |
|
223 Pure/Syntax/printer.ML:val show_markup_default = Unsynchronized.ref false; |
|
224 Pure/Syntax/printer.ML:val show_question_marks_default = Unsynchronized.ref true; |
|
225 Pure/Syntax/syntax_trans.ML:val eta_contract_default = Unsynchronized.ref true; |
|
226 Pure/Syntax/syntax_phases.ML: val reports = Unsynchronized.ref ([]: Position.report list); |
|
227 Pure/Syntax/syntax_phases.ML: val reports = Unsynchronized.ref reports0; |
|
228 Pure/Syntax/ast.ML: val passes = Unsynchronized.ref 0; |
|
229 Pure/Syntax/ast.ML: val failed_matches = Unsynchronized.ref 0; |
|
230 Pure/Syntax/ast.ML: val changes = Unsynchronized.ref 0; |
|
231 Pure/Proof/reconstruct.ML:val quiet_mode = Unsynchronized.ref true; |
|
232 Pure/Proof/extraction.ML: val cache = Unsynchronized.ref ([] : (term * term) list); |
|
233 Pure/Isar/runtime.ML:val debug = Unsynchronized.ref false; |
|
234 Pure/Isar/token.ML:fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE)) |
|
235 Pure/Isar/token.ML:fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v) |
|
236 Pure/Isar/toplevel.ML:val quiet = Unsynchronized.ref false; |
|
237 Pure/Isar/toplevel.ML:val interact = Unsynchronized.ref false; |
|
238 Pure/Isar/toplevel.ML:val timing = Unsynchronized.ref false; |
|
239 Pure/Isar/toplevel.ML:val profiling = Unsynchronized.ref 0; |
|
240 Pure/Isar/toplevel.ML:val skip_proofs = Unsynchronized.ref false; |
|
241 @ Pure/Isar/toplevel.ML: val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list); |
|
242 Pure/Isar/proof.ML: val testing = Unsynchronized.ref false; |
|
243 Pure/Isar/proof.ML: val rule = Unsynchronized.ref (NONE: thm option); |
|
244 Pure/Isar/outer_syntax.ML:val global_outer_syntax = Unsynchronized.ref empty_outer_syntax; |
|
245 Pure/Isar/keyword.ML: Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty)); |
|
246 |
|
247 --- ProofGeneral L"AUFT AUS ... |
|
248 Pure/ProofGeneral/proof_general_emacs.ML:val initialized = Unsynchronized.ref false; |
|
249 Pure/ProofGeneral/proof_general_pgip.ML:val pgmlsymbols_flag = Unsynchronized.ref true; |
|
250 Pure/ProofGeneral/proof_general_pgip.ML:val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref; |
|
251 Pure/ProofGeneral/proof_general_pgip.ML:val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref; |
|
252 Pure/ProofGeneral/proof_general_pgip.ML: val pgip_id = Unsynchronized.ref "" |
|
253 Pure/ProofGeneral/proof_general_pgip.ML: val pgip_seq = Unsynchronized.ref 0 |
|
254 Pure/ProofGeneral/proof_general_pgip.ML:val output_xml_fn = Unsynchronized.ref Output.physical_writeln |
|
255 Pure/ProofGeneral/proof_general_pgip.ML:val show_theorem_dependencies = Unsynchronized.ref false; |
|
256 Pure/ProofGeneral/proof_general_pgip.ML:val preferences = Unsynchronized.ref Preferences.pure_preferences; |
|
257 Pure/ProofGeneral/proof_general_pgip.ML:val currently_open_file = Unsynchronized.ref (NONE : pgipurl option) |
|
258 Pure/ProofGeneral/proof_general_pgip.ML:val initialized = Unsynchronized.ref false; |
|
259 Pure/ProofGeneral/proof_general_pgip.ML: val pgip_output_channel = Unsynchronized.ref Output.physical_writeln |
|
260 Pure/ProofGeneral/preferences.ML: 'a Unsynchronized.ref -> string -> string -> preference |
|
261 Pure/ProofGeneral/preferences.ML: val string_pref: string Unsynchronized.ref -> string -> string -> preference |
|
262 Pure/ProofGeneral/preferences.ML: val real_pref: real Unsynchronized.ref -> string -> string -> preference |
|
263 Pure/ProofGeneral/preferences.ML: val int_pref: int Unsynchronized.ref -> string -> string -> preference |
|
264 Pure/ProofGeneral/preferences.ML: val nat_pref: int Unsynchronized.ref -> string -> string -> preference |
|
265 Pure/ProofGeneral/preferences.ML: val bool_pref: bool Unsynchronized.ref -> string -> string -> preference |
|
266 |
|
267 Pure/term_sharing.ML: val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table); |
|
268 Pure/term_sharing.ML: val terms = Unsynchronized.ref (Syntax_Termtab.empty: unit Syntax_Termtab.table); |
|
269 Pure/term_subst.ML: let val maxidx = Unsynchronized.ref i |
|
270 Pure/term_subst.ML: let val maxidx = Unsynchronized.ref i |
|
271 Pure/term_subst.ML: | instantiateT_same instT ty = instT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty; |
|
272 Pure/term_subst.ML: | instantiate_same insts tm = inst_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm; |
|
273 Pure/pattern.ML:val trace_unify_fail = Unsynchronized.ref false; |
|
274 Pure/unify.ML: (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of |
|
275 Pure/unify.ML: if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN |
|
276 Pure/context.ML:val timing = Unsynchronized.ref false; |
|
277 Pure/context.ML: {self: theory Unsynchronized.ref option, (*dynamic self reference -- follows theory changes*) |
|
278 Pure/context.ML: SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) = |
|
279 Pure/context.ML: val r = Unsynchronized.ref thy; |
|
280 Pure/context.ML:fun deref (Theory_Ref (Unsynchronized.ref thy)) = thy; |
|
281 @ Pure/Concurrent/synchronized_sequential.ML:fun var _ x = Var (Unsynchronized.ref x); |
|
282 Pure/Concurrent/time_limit.ML: val timeout = Unsynchronized.ref false; |
|
283 Pure/Concurrent/synchronized.ML: var = Unsynchronized.ref x}; |
|
284 Pure/Concurrent/future.ML:val queue = Unsynchronized.ref Task_Queue.empty; |
|
285 Pure/Concurrent/future.ML:val next = Unsynchronized.ref 0; |
|
286 Pure/Concurrent/future.ML:val scheduler = Unsynchronized.ref (NONE: Thread.thread option); |
|
287 Pure/Concurrent/future.ML:val canceled = Unsynchronized.ref ([]: group list); |
|
288 Pure/Concurrent/future.ML:val do_shutdown = Unsynchronized.ref false; |
|
289 Pure/Concurrent/future.ML:val max_workers = Unsynchronized.ref 0; |
|
290 Pure/Concurrent/future.ML:val max_active = Unsynchronized.ref 0; |
|
291 Pure/Concurrent/future.ML:val worker_trend = Unsynchronized.ref 0; |
|
292 Pure/Concurrent/future.ML:val status_ticks = Unsynchronized.ref 0; |
|
293 Pure/Concurrent/future.ML:val last_round = Unsynchronized.ref Time.zeroTime; |
|
294 @ Pure/Concurrent/future.ML:val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list); |
|
295 Pure/Concurrent/future.ML:val ML_statistics = Unsynchronized.ref false; |
|
296 Pure/Concurrent/future.ML:val forked_proofs = Unsynchronized.ref 0; |
|
297 @ Pure/Concurrent/future.ML: Unsynchronized.ref Working)); |
|
298 Pure/Concurrent/lazy_sequential.ML:fun lazy e = Lazy (Unsynchronized.ref (Expr e)); |
|
299 Pure/Concurrent/lazy_sequential.ML:fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a))); |
|
300 Pure/General/secure.ML:val secure = Unsynchronized.ref false; |
|
301 Pure/General/pretty.ML:val margin_default = Unsynchronized.ref 76; (*right margin, or page width*) |
|
302 Pure/General/name_space.ML:val names_long_default = Unsynchronized.ref false; |
|
303 Pure/General/name_space.ML:val names_short_default = Unsynchronized.ref false; |
|
304 Pure/General/name_space.ML:val names_unique_default = Unsynchronized.ref true; |
|
305 Pure/General/position.ML: val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit |
|
306 Pure/General/print_mode.ML: val print_mode: string list Unsynchronized.ref (*global template*) |
|
307 Pure/General/print_mode.ML:val print_mode = Unsynchronized.ref ([]: string list); |
|
308 Pure/General/output.ML: val writeln_fn = Unsynchronized.ref physical_writeln; |
|
309 Pure/General/output.ML: val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); |
|
310 Pure/General/output.ML: val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s); |
|
311 Pure/General/output.ML: val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### "); |
|
312 Pure/General/output.ML: val error_fn = Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s)); |
|
313 Pure/General/output.ML: val prompt_fn = Unsynchronized.ref physical_stdout; |
|
314 Pure/General/output.ML: val status_fn = Unsynchronized.ref (fn _: output => ()); |
|
315 Pure/General/output.ML: val report_fn = Unsynchronized.ref (fn _: output => ()); |
|
316 Pure/General/output.ML: val result_fn = Unsynchronized.ref (fn _: serial * output => ()); |
|
317 Pure/General/output.ML: val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref = |
|
318 @ Pure/General/output.ML: Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode"); |
|
319 Pure/Tools/find_theorems.ML:val tac_limit = Unsynchronized.ref 5; |
|
320 Pure/Tools/find_theorems.ML:val limit = Unsynchronized.ref 40; |
|
321 Pure/raw_simplifier.ML:val simp_trace_depth_limit_default = Unsynchronized.ref 1; |
|
322 Pure/raw_simplifier.ML: if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context)); |
|
323 Pure/raw_simplifier.ML:val simp_trace_default = Unsynchronized.ref false; |
|
324 Pure/raw_simplifier.ML: make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE), |
|
325 Pure/raw_simplifier.ML:val debug_bounds = Unsynchronized.ref false; |
|
326 Pure/ROOT.ML:val quick_and_dirty = Unsynchronized.ref false; |
|
327 Pure/goal_display.ML:val goals_limit_default = Unsynchronized.ref 10; |
|
328 Pure/goal_display.ML:val show_main_goal_default = Unsynchronized.ref false; |
|
329 Pure/goal_display.ML:val show_consts_default = Unsynchronized.ref false; |
|
330 Pure/ML/ml_compiler_polyml.ML: Unsynchronized.ref (toks |> map |
|
331 Pure/ML/ml_compiler_polyml.ML: val writeln_buffer = Unsynchronized.ref Buffer.empty; |
|
332 Pure/ML/ml_compiler_polyml.ML: val warnings = Unsynchronized.ref ([]: string list); |
|
333 Pure/ML/ml_compiler_polyml.ML: val error_buffer = Unsynchronized.ref Buffer.empty; |
|
334 @ Pure/goal.ML:val parallel_proofs = Unsynchronized.ref 1; |
|
335 Pure/goal.ML:val parallel_proofs_threshold = Unsynchronized.ref 50; |
|
336 Pure/tactical.ML: val tracify: bool Unsynchronized.ref -> tactic -> tactic |
|
337 Pure/tactical.ML:val trace_REPEAT= Unsynchronized.ref false |
|
338 Pure/tactical.ML:and suppress_tracing = Unsynchronized.ref false; |
|
339 Pure/type.ML: val tyvar_count = Unsynchronized.ref maxidx; |
|
340 @ Pure/PIDE/document.ML: (no_id, Future.new_group NONE, Unsynchronized.ref false)); |
|
341 @ Pure/PIDE/document.ML: val execution' = (id, Future.new_group NONE, Unsynchronized.ref true); |
|
342 Pure/PIDE/document.ML:val timing = Unsynchronized.ref false; |
|
343 Pure/search.ML:val trace_DEPTH_FIRST = Unsynchronized.ref false; |
|
344 Pure/search.ML: let val countr = Unsynchronized.ref 0 |
|
345 Pure/search.ML:val trace_DEEPEN = Unsynchronized.ref false; |
|
346 Pure/search.ML:val trace_BEST_FIRST = Unsynchronized.ref false; |
|
347 Pure/search.ML:val trace_ASTAR = Unsynchronized.ref false; |
|
348 Pure/Thy/thy_output.ML:val display_default = Unsynchronized.ref false; |
|
349 Pure/Thy/thy_output.ML:val quotes_default = Unsynchronized.ref false; |
|
350 Pure/Thy/thy_output.ML:val indent_default = Unsynchronized.ref 0; |
|
351 Pure/Thy/thy_output.ML:val source_default = Unsynchronized.ref false; |
|
352 Pure/Thy/thy_output.ML:val break_default = Unsynchronized.ref false; |
|
353 Pure/Thy/thy_output.ML:val modes = Unsynchronized.ref ([]: string list); |
|
354 Pure/Thy/thy_load.ML: val master_path = Unsynchronized.ref Path.current; |
|
355 Pure/Thy/present.ML:val browser_info = Unsynchronized.ref empty_browser_info; |
|
356 Pure/Thy/present.ML:val suppress_tex_source = Unsynchronized.ref false; |
|
357 Pure/Thy/present.ML:val session_info = Unsynchronized.ref (NONE: session_info option); |
|
358 Pure/Thy/thy_info.ML: Unsynchronized.ref (String_Graph.empty: (deps option * theory option) String_Graph.T); |
|
359 @ Pure/proofterm.ML:val proofs = Unsynchronized.ref 2; |
|
360 |
|
361 --- Tools concerns external provers, Isac shall use in the future --- thus observe conflicts |
|
362 Sequents/prover.ML:val trace = Unsynchronized.ref false; |
|
363 Tools/Code/code_runtime.ML:val trace = Unsynchronized.ref false; |
|
364 Tools/WWW_Find/scgi_server.ML:val max_threads = Unsynchronized.ref 5; |
|
365 Tools/WWW_Find/scgi_server.ML:val servers = Unsynchronized.ref (Symtab.empty : (Mime.t option * handler) Symtab.table); |
|
366 Tools/WWW_Find/scgi_server.ML: val threads = Unsynchronized.ref ([] : Thread.thread list); |
|
367 Tools/misc_legacy.ML:val gensym_seed = Unsynchronized.ref (0: int); |
|
368 Tools/Metis/metis.ML:local val rand = (*Unsynchronized.*)Unsynchronized.ref 0w1 |
|
369 Tools/Metis/metis.ML:val withRef : 'r Unsynchronized.ref * 'r -> ('a -> 'b) -> 'a -> 'b |
|
370 Tools/Metis/metis.ML: val tracePrint = Unsynchronized.ref tracePrintFn; |
|
371 Tools/Metis/metis.ML: val generator = Unsynchronized.ref 0 |
|
372 Tools/Metis/metis.ML:fun quickly v = Metis_Lazy (Unsynchronized.ref (Value v)); |
|
373 Tools/Metis/metis.ML:fun delay f = Metis_Lazy (Unsynchronized.ref (Thunk f)); |
|
374 Tools/Metis/metis.ML: val cache = Unsynchronized.ref (Metis_Map.new cmp) |
|
375 Tools/Metis/metis.ML:val lineLength = Unsynchronized.ref initialLineLength; |
|
376 Tools/Metis/metis.ML: val lastLine = Unsynchronized.ref (~1,"","","") |
|
377 Tools/Metis/metis.ML: val Unsynchronized.ref (n,_,l2,l3) = lastLine |
|
378 Tools/Metis/metis.ML: val Unsynchronized.ref (n,l1,l2,l3) = lastLine |
|
379 Tools/Metis/metis.ML: (Unsynchronized.ref o Metis_Print.Infixes) |
|
380 Tools/Metis/metis.ML:val negation : string Unsynchronized.ref = Unsynchronized.ref "~"; |
|
381 Tools/Metis/metis.ML:val binders : string list Unsynchronized.ref = Unsynchronized.ref ["\\","!","?","?!"]; |
|
382 Tools/Metis/metis.ML:val brackets : (string * string) list Unsynchronized.ref = Unsynchronized.ref [("[","]"),("{","}")]; |
|
383 Tools/Metis/metis.ML: val Unsynchronized.ref s = Metis_Term.negation |
|
384 Tools/Metis/metis.ML: val counter : int Metis_StringMap.map Unsynchronized.ref = Unsynchronized.ref (Metis_StringMap.new ()); |
|
385 Tools/Metis/metis.ML: val Unsynchronized.ref m = counter |
|
386 Tools/Metis/metis.ML: val counter : int Unsynchronized.ref = Unsynchronized.ref 0; |
|
387 Tools/Metis/metis.ML: val Unsynchronized.ref i = counter |
|
388 Tools/Metis/metis.ML: tableMap = Unsynchronized.ref (Metis_NameArityMap.new ())}; |
|
389 Tools/Metis/metis.ML: val Unsynchronized.ref m = tm |
|
390 Tools/Metis/metis.ML: val r = Unsynchronized.ref 0 |
|
391 Tools/Metis/metis.ML: val Unsynchronized.ref n = r |
|
392 Tools/Metis/metis.ML:val showId = Unsynchronized.ref false; |
|
393 |
|
394 Tools/coherent.ML:val verbose = Unsynchronized.ref false; |
|
395 Tools/coherent.ML:val show_facts = Unsynchronized.ref false; |
|
396 Tools/nbe.ML:val trace = Unsynchronized.ref false; |
|
397 Tools/quickcheck.ML: val add_timing : (string * int) -> result Unsynchronized.ref -> unit |
|
398 Tools/quickcheck.ML: val add_response : string list -> term list -> (bool * term list) option -> result Unsynchronized.ref -> unit |
|
399 Tools/quickcheck.ML: val add_report : int -> report option -> result Unsynchronized.ref -> unit |
|
400 Tools/quickcheck.ML:val auto = Unsynchronized.ref false; |
|
401 Tools/solve_direct.ML:val auto = Unsynchronized.ref false; |
|
402 Tools/solve_direct.ML:val max_solutions = Unsynchronized.ref 5; |
|
403 Tools/try.ML:val auto_time_limit = Unsynchronized.ref 4.0 |
|
404 |
|
405 Tools/isac/Frontend/states.sml:val states = Unsynchronized.ref ([]:(iterID * (calcID * state) list) list); |
|
406 !! Tools/isac/calcelems.sml:val theory' = Unsynchronized.ref ([]:(theory' * theory) list); |
|
407 !! Tools/isac/calcelems.sml:val isabthys = Unsynchronized.ref ([] : theory list); |
|
408 !! Tools/isac/calcelems.sml:val knowthys = Unsynchronized.ref ([] : theory list); |
|
409 !! Tools/isac/calcelems.sml:val progthys = Unsynchronized.ref ([] : theory list); |
|
410 !! Tools/isac/calcelems.sml:val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list); |
|
411 !! Tools/isac/calcelems.sml:val calclist'= Unsynchronized.ref ([]: calc list); |
|
412 !! Tools/isac/calcelems.sml:val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*) |
|
413 !! Tools/isac/calcelems.sml:val isab_thm_thy = Unsynchronized.ref ([] : (thmDeriv * term) list); |
|
414 !! Tools/isac/calcelems.sml:val isabthys = Unsynchronized.ref ([] : theory list); |
|
415 !! Tools/isac/calcelems.sml:val first_ProgLang_thy = Unsynchronized.ref (@{theory Pure}); |
|
416 !! Tools/isac/calcelems.sml:val first_Knowledge_thy = Unsynchronized.ref (@{theory Pure}); |
|
417 Tools/isac/calcelems.sml:val trace_rewrite = Unsynchronized.ref false; |
|
418 Tools/isac/calcelems.sml:val depth = Unsynchronized.ref 99999; |
|
419 Tools/isac/calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999; |
|
420 Tools/isac/calcelems.sml:val lim_deriv = Unsynchronized.ref 100; |
|
421 Tools/isac/calcelems.sml:val check_guhs_unique = Unsynchronized.ref true; |
|
422 !? Tools/isac/ProgLang/Script.thy:val tacs = Unsynchronized.ref (distinct (remove op = "" |
|
423 !? Tools/isac/ProgLang/Script.thy:val screxpr = Unsynchronized.ref (distinct (remove op = "" |
|
424 !? Tools/isac/ProgLang/Script.thy:val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *) |
|
425 !? Tools/isac/ProgLang/Script.thy:val scrfuns = Unsynchronized.ref ([]: string list); |
|
426 !? Tools/isac/ProgLang/Script.thy:val listexpr = Unsynchronized.ref (union op = (!listfuns) (!scrfuns)); |
|
427 !? Tools/isac/ProgLang/Script.thy:val notsimp = Unsynchronized.ref |
|
428 !? Tools/isac/ProgLang/Script.thy:val negotiable = Unsynchronized.ref ((!tacs (*@ !subpbls*))); |
|
429 Tools/isac/Knowledge/GCD_Poly_ML.thy: val trace_div = Unsynchronized.ref true; |
|
430 Tools/isac/Knowledge/GCD_Poly_ML.thy: val trace_div_invariant = Unsynchronized.ref false; (*.. true expects !trace_div = false *) |
|
431 Tools/isac/Knowledge/GCD_Poly_ML.thy: val trace_Euclid = Unsynchronized.ref true; |
|
432 !! Tools/isac/Interpret/inform.sml:val castab = Unsynchronized.ref ([]: castab); |
|
433 Tools/isac/Interpret/script.sml:val trace_script = Unsynchronized.ref false; |
|
434 !! Tools/isac/Interpret/ptyps.sml:val pbltypes = Unsynchronized.ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*) |
|
435 !! Tools/isac/Interpret/ptyps.sml:val ptyps = Unsynchronized.ref ([e_Ptyp]:ptyps); |
|
436 !! Tools/isac/Interpret/ptyps.sml:val mets = Unsynchronized.ref ([e_Mets]:mets); |
|
437 Tools/isac/Interpret/ctree.sml:> val pt = Unsynchronized.ref EmptyPtree; |
|
438 !? Tools/isac/Interpret/ctree.sml: val pt = Unsynchronized.ref Empty; |
|
439 |
|
440 ZF/ind_syntax.ML:val trace = Unsynchronized.ref false; |
|
441 ZF/Datatype_ZF.thy: val trace = Unsynchronized.ref false; |
|