[isabelle-dev] Performance problem with AFP/Network_Security_Policy_Verification (theory Code_Char)
Makarius
makarius at sketis.net
Sat Feb 3 15:32:00 CET 2018
The following performance problem with
AFP/Network_Security_Policy_Verification has shown up in the past few days:
Isabelle/a7de81d847b0, AFP/455f23697b09, lxbroy10, x86-linux, threads=6
Finished Network_Security_Policy_Verification (0:03:51 elapsed time,
0:18:22 cpu time, factor 4.77)
Isabelle/c555f1778dd8, AFP/a6e1af6e0ad2, lxbroy10, x86-linux, threads=6
Finished Network_Security_Policy_Verification (0:13:12 elapsed time,
0:47:23 cpu time, factor 3.59)
Detailed results from profiling=time are included. Here are the relevant
bits.
log1:
3209 eq-typ
3388 Table().modify
3875 Table().defined
4121 Generated_Code.filter
6297 Table().lookup_key
7364 GARBAGE COLLECTION (minor collection)
8350 GARBAGE COLLECTION (total)
log2:
2959 eq-typ
3429 Table().modify
3998 Table().defined
4648 Generated_Code.filter
6098 Table().lookup
7989 GARBAGE COLLECTION (minor collection)
8928 GARBAGE COLLECTION (total)
13544 Generated_Code.equal_chara
29343 Generated_Code.divmod_integer
45490 IntInf.divMod
69982 Generated_Code.numeral
It appears to be related to changeset:
8853:2f3bdae911bb
user: haftmann
date: Mon Jan 29 19:38:17 2018 +0000
files: thys/Algebraic_Numbers/Algebraic_Number_Tests.thy
thys/Linear_Recurrences/Linear_Recurrences_Test.thy
thys/Network_Security_Policy_Verification/Lib/Efficient_Distinct.thy
thys/Network_Security_Policy_Verification/Lib/FiniteListGraph_Impl.thy
thys/Polynomial_Factorization/ROOT
thys/QR_Decomposition/Examples_QR_Abstract_Symbolic.thy
thys/QR_Decomposition/Examples_QR_IArrays_Symbolic.thy
thys/Regex_Equivalence/Regex_Equivalence.thy
description:
removed superflous imports of theory Code_Char
Makarius
-------------- next part --------------
Network_Security_Policy_Verification:
1 Thm.instantiate'
1 Proof.append_using
1 Meson.skolemize_prems_tac
1 Graph().map_strong_conn
1 ATP_Problem.formula_fold
1 Code_Preproc.add_classes
1 Global_Theory.name_multi
1 Scan.provide
1 Code_Preproc.add_styp
1 Facts.retrieve
1 CODEGEN_PARSETREE().codeNonRecValBindings
1 Lin_Arith.LA_Logic.neg_prop
1 Thread_Attributes.expose_interrupt
1 Proofterm.strip_shyps_proof
1 Toplevel.node_of
1 tabulate'
1 ExportTree().exportNavigationProps
1 Consts.typargs
1 Name_Space.make_accesses
1 Local_Theory.assert
1 Thy_Syntax.flat_element
1 Logic.remove_params
1 Lin_Arith.LA_Data.subst_term
1 Blast().addLit
1 Local_Theory.map_top
1 Thm.rule_attribute
1 Code_Printer.intro_base_names_for
1 Syntax_Phases.unparse_t
1 Output_Primitives.ignore_outputs
1 VALUE_OPS().makeLocalV
1 Metis_TermNet.norm
1 CODETREE_CODEGEN_CONSTANT_FUNCTIONS().codeGenerate
1 String.convString
1 Cancel_Div_Mod().proc
1 Tactic.insert_tagged_brl
1 Simplifier_Trace.indicate_failure
1 String.tokens
1 EqSubst.mk_foo_match
1 Thy_Output.present_token
1 CODEGEN_PARSETREE().codeMatch
1 Library.list_ord
1 Calculation.update_calculation
1 Name.bound
1 Graph().merge_trans_acyclic
1 BNF_Def.prepare_def
1 STRUCTURES_().pass4Structs
1 Metis_Active.simplify
1 Name.enforce_case'
1 Code.get_cert
1 Code.merge_specs
1 Drule.strip_imp_prems
1 Code.devarify
1 Boolean_Algebra_Cancel.cancel_conv
1 Library.funpow
1 Metis_Thm.equality
1 Metis_TermNet.add
1 Seq.mapp
1 Bundle.gen_activate
1 TYPE_TREE().assignTypes
1 Outer_Syntax.parse_tokens
1 CODETREE_OPTIMISER().mapCodeForFunctionRewriting
1 Consts.the_const
1 ExportTree().exportList
1 Generic_Target.notes
1 Metis_Clause.isLargerLiteral
1 Blast().traceVars
1 Future.scheduler_next
1 Search.DEPTH_FIRST
1 Code.rewrite_eqn
1 Code_Preproc.trans_comb
1 PolyML.prettyMarkup
1 Code.is_linear
1 Term.loose_bvar1
1 Task_Queue.enqueue
1 Name_Space.entry_markup
1 X86OUTPUTCODE().rtsCall
1 BinIO.openOut
1 EqSubst.fakefree_badbounds
1 CODETREE_SIMPLIFIER().mkEnv
1 Lin_Arith.add_arith_facts
1 it-setup
1 Orders.order_tac
1 Blast().delete_concl
1 Thm.strip_apply
1 Conv.abs_conv
1 Local_Theory.background_theory_result
1 Variable.declare_constraints
1 DEBUGGER_().wrapFunctionInDebug
1 STRUCTURES_().pass2Struct
1 Position.here
1 Scan.one
1 Outer_Syntax.ship
1 Code.concretify_abs
1 Assumption.map_data
1 Unify.add_tpair
1 Graph().del_node
1 Parser.get_states
1 Trancl_Tac().rtrancl_tac
1 Scan.dest
1 Record.get_update_details
1 Markup.language'
1 Code.raw_assert_eqn
1 Syntax_Phases.check
1 Keyword.merge_keywords
1 ProofRewriteRules.rew
1 Thm.legacy_freezeT
1 Future.assign_result
1 Term.strip_all_vars
1 Name_Space.alias
1 Parse.keyword_markup
1 ATP_Problem_Generate.introduce_proxies_in_iterm
1 Variable.constrain_tvar
1 Element.satisfy_thm
1 Metis_Reconstruct.one_step
1 eq-tree
1 Token.is_eof
1 Proof.assert_mode
1 Blast().match
1 Thread_Position.setmp
1 Code.const_typ_eqn
1 Syntax.apply_tr'
1 Order_Tac.mkasm_partial
1 Assumption.export
1 List.last
1 IntInf.divMod
1 X86OUTPUTCODE().opRegPlus2
1 Metis_Rule.fact
1 StringCvt.scanString
1 Library.read_radix_int
1 Token.stopper
1 Local_Defs.meta_rewrite_conv
1 Term.no_dummy_patterns
1 Private_Output.default_output
1 Function_Core.prove_stuff
1 Goal.PREFER_GOAL
1 Syntax_Phases.parse_term
1 LEX_().parseString
1 Metis_Rewrite.neqConvsAdd
1 Toplevel.element_result
1 Balanced_Tree.dest
1 Exn.interruptible_capture
1 Induct().atomize_tac
1 DATATYPE_REP().chooseConstrRepr
1 Context.Proof_Data.put
1 Trancl_Tac.decomp
1 Metis_Map.treeAppend
1 Metis_Subst.compatible
1 Tactical.COND
1 ML_Syntax.print_pair
1 Thm.abstract_rule
1 Syntax_Phases.ast_to_term
1 CODETREE_SIMPLIFIER().simpAddress
1 Par_Exn.release_first
1 Code_ML.serialize_ml
1 Unify.get_eta_var
1 Tactical.ALLGOALS
1 Options.check_type
1 Metis_KeyMap().treeMap
1 Isar_Cmd.terminal_proof
1 Metis_Rule.rewrConv
1 TYPEIDCODE().equalityForDatatypes
1 CODETREE_FUNCTIONS().findEntryInBlock
1 Classical().add_safe_elim
1 Proof_Context.check_const
1 Conjunction.elim
1 Term.size_of_term
1 Thm.theory_of_thm
1 HOLogic.dest_numeral
1 Item_Net.retrieve_matching
1 Code_Scala.print_scala_stmt
1 Context_Position.reported_text
1 Fast_Lin_Arith().mklineq
1 Thm.weaken_sorts
1 Envir.subst_type
1 Method.method
1 Code_Preproc.switch_trace
1 eq-T
1 Ast.fold_ast
1 Library.single
1 Term.fold_subtypes
1 Parser.movedot_lambda
1 TYPE_TREE().copyTypeConstrWithCache
1 Thm.flexflex_rule
1 Method.insert_tac
1 Global_Theory.name_thm
1 VALUE_OPS().applyFunction
1 Symbol.is_ascii_identifier
1 Raw_Simplifier.orient_rrule
1 Syntax_Phases.ast_of_termT
1 VALUE_OPS().codeVal
1 Seq.map
1 SIGNATURES().sigVal
1 Value.parse_bool
1 CODETREE().bottomLevel
1 Raw_Simplifier.generic_rewrite_goal_tac
1 Term.binder_types
1 Numeral_Simprocs.numterms_ord
1 Metis_ElementSet().firstl
1 Future.interruptible_task
1 Code_Preproc.ensure_inst
1 Blast().TRACE
1 Lexicon.literal_markup
1 X86OUTPUTCODE().opReg
1 Named_Target.init'
1 ProtectedTable.lookup
1 Lazy.force
1 Asn1.readHeader
1 Classical().inst0_step_tac
1 Thy_Output.ignore
1 Toplevel.skip_proof_close
1 Isabelle1067944.map
1 Lin_Arith.LA_Data.pre_tac
1 Inductive.prove_mono
1 Library.pair
1 Code_Namespace.prep_symbol
1 Proofterm.unconstrainT_prf
1 Assumption.add_assms
1 Metis_KnuthBendixOrder.add
1 Unify.smash_flexflex
1 Same.same
1 List_to_Set_Comprehension.dest_case
1 Unify.flexargs
1 Token.space_symbol
1 Fast_Lin_Arith().print_ineqs
1 Library.unprefix
1 Proof_Context.gen_cert
1 Lin_Arith.LA_Logic.atomize
1 Symbol.spaces
1 Hypsubst().vars_gen_hyp_subst_tac
1 Term.loose_bvar
1 Future.promise_name
1 Metis_Rule.pathLiterule
1 CODEGEN_PARSETREE().codeLambda
1 Code_ML.literals_sml
1 Envir.subst_type0
1 Metis_TermNet.termToQterm
1 Order_Tac.mkconcl_partial
1 TYPE_TREE().checkForEscapingDatatypes
1 Metis_Rule.allArgumentsLiterule
1 STRUCT_VALS().makeLook
1 Binding.default_pos
1 Code_Thingol.translate_dicts
1 Thm.major_prem_of
1 Function_Mutual.in_context
1 Misc.lookupDefault
1 Resources.theory_name
1 Metis_KeyMap().treePeekPath
1 Defs.disjoint_specs
1 PolyRealBoxedToString
1 Goal.prove_common
1 TYPECHECK_PARSETREE().setLeastGeneralTypes
1 Code.equations_of_cert
1 Blast().fromIntrRule
1 Thy_Info.excursion
1 Metis_Subsume.insert
1 Code_Evaluation.subst_termify
1 Function_Core.mk_partial_induct_rule
1 Scan.depend
1 EqSubst.clean_unify
1 Code.typscheme
1 Generated_Code.trancl_impl
1 CODETREE().newLevel
1 DEBUGGER_().breakPointCode
1 Metis_KnuthBendixOrder.compare
1 Numeral_Simprocs.numterm_ord
1 Proof_Context.Data.init
1 Class.all_assm_intros
1 Future.fulfill_result
1 Library.nth
1 Metis_TermNet.computeSize
1 Symbol.bump_init
1 Classical().add_unsafe_intro
1 Table().lookup_list
1 CODETREE_FUNCTIONS().makeConstVal
1 Proof_Context.update_case
1 Real.fmt
1 Simplifier_Trace.indicate_success
1 CODEGEN_PARSETREE().codeSequence
1 Logic.mk_arities
1 Function_Common.transform_function_data
1 Ctr_Sugar_Util.ss_only
1 UniversalTable.fold
1 Proof_Context.update_thms
1 Toplevel.presentation_context
1 Metis_KnuthBendixOrder.weightLowerBound
1 CODEGEN_PARSETREE().tupleWidth
1 Blast().eta_contract_atom
1 Thm.check_hyps
1 Raw_Simplifier.is_full_cong
1 Antiquote.scan_txt
1 Rule_Cases.make
1 TYPE_TREE().displayTypeConstrsWithMap
1 Symbol.is_ascii_upper
1 Misc.quickSort
1 Lexicon.tokenize
2 Future.worker_exec
2 Comment.read_body
2 Metis_Rule.everyConv
2 Future.worker_start
2 Metis_Units.reduce
2 Name_Space.check_reports
2 Logic.lift_abs
2 Library.chop_common_prefix
2 X86OUTPUTCODE().opCodeBytes
2 Code.const_typ
2 Toplevel.atom_result
2 Metis_Subsume.nonunitSubsumes
2 Antiquote.scan_antiq
2 Envir.vupdate
2 Term_Ord.types_ord
2 CODETREE_OPTIMISER().optLambda
2 UTILITIES_().searchList
2 Blast().prune
2 Drule.lift_all
2 Proof_Context.note_thmss
2 Proof.terminal_proof
2 Class.synchronize_class_syntax
2 List.tabF
2 CODETREE_OPTIMISER().useToPattern
2 CombineNumeralsFun().proc
2 BasicStreamIO().flushOut'
2 Thm.dest_abs
2 Context.Proof_Context.init_global
2 Method.sect
2 Metis_Atom.subterm
2 Thm.assume_hyps
2 Lin_Arith.LA_Data.filter_prems_tac_items
2 PRINT_TABLE().getOverloads
2 Library.chop
2 HashTable.fold
2 Proof_Context.retrieve
2 Envir.binder_types
2 Drule.zero_var_indexes_list
2 Pretty.newline
2 Thm.apply
2 Fast_Lin_Arith().refutes
2 TYPEIDCODE().printerForDatatype
2 Toplevel.apply_tr
2 ZipperFUN().lzy_search
2 polyCompiler
2 MATCH_COMPILER().plus
2 Printer.show_markup_raw
2 Simplifier_Trace._
2 Metis_Thm.chk
2 Unify.sort_args
2 Symbol_Pos.source
2 BNF_Tactics.mk_pointfree2
2 Variable.declare_names
2 Outer_Syntax.parse
2 Syntax.read_terms
2 Proof_Context.def_type
2 Local_Theory.standard_morphism
2 CODETREE_STATIC_LINK_AND_CASES().codeGenerate
2 YXML.push
2 Parse.arguments
2 Parser.produce
2 Lexicon.scan_vname-chop_idx
2 Thm.add_inst
2 Metis_Generate.reveal_old_skolem_terms
2 Element.map_ctxt
2 Morphism.compose
2 Code_Printer.gen_print_app
2 Latex.output_sym
2 Hypsubst().eq_var
2 Net.dest
2 CODETREE_FUNCTIONS().setInline
2 PolyFloatArbitraryPrecision
2 Code_Printer.printer_of_mixfix
2 X86OUTPUTCODE().getConstant
2 Toplevel.setmp_thread_position
2 Code_Thingol.ensure_class
2 Simpdata.mk_atomize
2 Blast().wkNormAux
2 Calculation.collect
2 Splitter().cmap_of_split_thms
2 Token.check_src
2 Symbol.beginning
2 Spec_Rules.Rules.empty
2 Code_Printer.make_vars
2 Generated_Code.sinvara
2 Basics.#->
2 STRUCTURES_().gencodeStructs
2 Tactical.REPEAT_DETERM_N
2 Thy_Output.present_thy
2 Term.typ_subst_TVars
2 Simplifier_Trace.check_breakpoint
2 CancelNumeralsFun().proc
2 Term.add_tfreesT
2 Local_Theory.map_contexts
2 Code.History.merge_history
2 Conv.combination_conv
2 Latex.output_name
2 Code_Thingol.unfoldl
2 Path.eval
2 Future.signal
2 Code_Symbol.prefix
2 SKIPS_().getsym
2 X86ICodeTransform().codeICodeFunctionToX86
2 String.concatWith
2 Lin_Arith.LA_Data.add_atom
2 Generated_Code.sinvar
2 Simpdata.unsafe_solver_tac
2 Hypsubst().gen_hyp_subst_tac
2 Axclass.overload_conv
2 Proof.global_goal
2 Thm.derivation_name
2 Element.transform_ctxt
2 Raw_Simplifier.congc
2 Fast_Lin_Arith().prove
2 Misc_Legacy.add_typ_tvars
2 Code_Preproc.styp_of
2 Library.downto
2 Variable.invent_types
2 YXML.pop
2 Syntax_Phases.simple_ast_of
2 Thm.beta_conversion
2 Metis_Rewrite.rewrIdConv'
2 Toplevel.app
2 Timing.protocol_message
2 Pretty.enclose
2 Metis_Subsume.unitSubsumes
2 Proof_Context.export_binds
2 MATCH_COMPILER().buildAot
2 ListPair.zip
2 Attrib.attribute_syntax
2 ListPair.unzip
2 Tactic.biresolution_from_nets_tac
2 Simplifier_Trace.step
2 Consts.empty_abbrevs
2 Proof_Context.expand_binds
2 Proof_Context.gen_fixes
2 Parse.group
3 Term.strip_abs_eta
3 AList.map_index
3 Thm.rename_bvs
3 Task_Queue.ready_job
3 Symbol_Pos.stopper
3 Proofterm.promise_proof
3 Parse.cut
3 eq-xsymb
3 CODETREE_SIMPLIFIER().simpUnary
3 Locale.witness_add
3 Theory.check_def
3 Code_Symbol.default_base
3 Numeral.dest_num
3 Table().map_entry
3 Config.declare_option
3 Graph().irreducible_paths
3 ML_Pretty.from_polyml-convert
3 Logic.unvarifyT_global_same
3 Library.nth_map
3 Code.same_arity
3 StronglyConnected.stronglyConnectedComponents
3 LEX_().parseIdent
3 Options.get
3 Name_Space.naming_of
3 Variable.def_type
3 Type.change_ignore
3 Metis_Rewrite.rewriteIdLiteralsRule'
3 Conv.fconv_rule
3 UTILITIES_().checkForDots
3 Drule.comp
3 CODETREE_SIMPLIFIER().simplifier
3 Thm.forall_elim
3 Code_Preproc.ensure_fun
3 Metis_Waiting.add'
3 Metis_Rule.transEqn
3 Variable.add_fixes_binding
3 Metis_Rule.firstConv
3 TYPE_TREE().allowGeneralisation
3 Code_Preproc.obtain_eqns
3 CODETREE_CODEGEN_CONSTANT_FUNCTIONS().cgLambda
3 Method.evaluate
3 eq-loadForm
3 eq-kind
3 Thy_Header.read_header
3 Library.map_index
3 Drule.beta_eta_conversion
3 MATCH_COMPILER().codeMatchPatterns
3 Token.map_value
3 Thy_Syntax.map_element
3 Tactical.EVY
3 Code_ML.ml_program_of_program
3 Term.map_type_tfree
3 Meson.protect_bound_var_names
3 Code.cert_of_eqns
3 Lin_Arith.LA_Data.allows_lin_arith
3 Syntax.apply_ast_tr'
3 Variable.import_inst
3 Thm.implies_elim
3 Thm.dest_comb
3 Address.stringOfWord
3 Tactical.ORELSE
3 Tactical.THEN'
3 Raw_Simplifier.simp_trace_raw
3 Raw_Simplifier.check_conv
3 Latex.output_chr
3 CODEGEN_PARSETREE().codeFunBindings
3 Metis_Subsume.genClauseSubsumes
3 Unify.matchers
3 STRUCT_VALS().makeEnv
3 Properties.seconds
3 CODETREE_FUNCTIONS().codeProps
3 Toplevel.transition
3 Metis_Rule.pathConv
3 Envir.insert_sorts
3 Tactical.THEN
3 Code.check_decl_ty
3 Pattern.flexflex2
3 Axclass.get_info
3 Unify.rigid_bound
3 Binding.check
3 Library.prefix
3 Library.upto
3 ML_Compiler.report_parse_tree
3 Task_Queue.dequeue_deps
3 Metis_Rule.repeatConv
4 Scan.literal
4 X86OUTPUTCODE().opToInt
4 Sorts.witness_sorts
4 Execution.fork
4 Logic.flatten_params
4 Scan.first
4 Metis_KeyMap().treeUnionDomain
4 Value.parse_int
4 Metis_Map.treeIntersectDomain
4 Envir.decr
4 Blast().strip_imp_prems
4 LEX_().isAlphaNumeric
4 Metis_Tactic.kbo_advisory_simp_ordering
4 BasicStreamIO().input'
4 CODEGEN_PARSETREE().reportUnreferencedValue
4 Syntax_Phases.decode_term
4 Code_Preproc.get_node
4 Code_Thingol.ensure_const
4 Library.replicate_string
4 Metis_Atom.match
4 Token.is_symid
4 Simplifier_Trace.recurse
4 Thm.varifyT_global'
4 Simplifier.generic_simp_tac
4 Envir.eta
4 Metis_Useful.sort
4 Thy_Output.output_token
4 YXML.string_of_body
4 Seq.list_of
4 Fast_Lin_Arith().simpset_lin_arith_tac
4 Metis_TermNet.qm
4 Logic.unconstrainT
4 Pattern.mapbnd
4 Ast.match
4 Lin_Arith.LA_Data.decomp_negation
4 Library.map2
4 Code_Evaluation.subst_termify_app
4 Code.add_rhss_of_eqn
4 PRINT_TABLE().getOverload
4 exists_p_split
4 Thm.forall_intr
4 IntSet.addItem
4 Element.instantiate_tfrees
4 Lin_Arith.LA_Data.pre_decomp
4 Conv.gconv_rule
4 Name_Space.intern'
4 Future.future_job
4 Proof_Context.map_data_result
4 TYPEIDCODE().TypeVarMap.mapTypeVars
4 UTILITIES_().noDuplicates
4 Blast().varOccur
4 Thm.generalize
4 Defs.merge
4 Thm.incr_indexes
4 Thm.equal_elim
5 Command.read
5 Context.init_new_data
5 Pretty.force_next
5 HashTable.hashSet
5 List.concat
5 it-proc
5 Term.map_aterms
5 Variable.gen_all
5 Code_Thingol.translate_app
5 Token.syntax_generic
5 Context.invoke
5 Syntax_Phases.parsetree_to_ast
5 Proofterm.add_npvars'
5 EXPORT_PARSETREE().getExportTree
5 Code.eqn_conv
5 Term.declare_typ_names
5 Ctr_Sugar.morph_ctr_sugar
5 Ast.normalize
5 Generated_Code.nonInterference_host_attributes
5 Tactical.ORELSE'
5 Thm.plain_prop_of
5 Blast().fromType
5 TYPE_TREE().tDisp
5 Code_Preproc.const_ord
5 Code_Namespace.hierarchical_program
5 Toplevel.apply_union
5 Rat.make
5 Term_Subst.zero_var_inst
5 Metis_Atom.unify
5 Type_Infer_Context.prepare
5 Thm.permute_prems
5 Code_Printer.intro_base_names
5 Term.incr_bv
5 Char.contains
5 Order_Tac.mkasm_linear
5 Morphism.app
5 Simpdata.mk_eq
6 Seq.chop
6 Build.protocol_message
6 X86OUTPUTCODE().largeWordToBytes
6 LEX_().readChars
6 BinIO.openIn
6 Term.subst_bounds
6 Type.varify_global
6 Thm.strip_shyps
6 TYPE_TREE().compareLabels
6 Generated_Code.netModel_node_props
6 Axclass.insert_arity_completions
6 Unify.clean_term
6 Unify.SIMPL
6 Unify.change_bnos
6 Envir.body_type
6 Generated_Code.netModel_node_propsa
6 HashTable.hashValue
6 Proof_Context.prepare_patternT
6 exists_paired_all
6 Consts.the_constraint
6 Logic.strip_params
6 Syntax_Phases.simple_check
6 Type_Infer_Context.prepare_positions
6 Term_Subst.map_aterms_same
6 SymSet.++
6 Lin_Arith.LA_Data.decomp_typecheck
6 Simplifier_Trace.simp_apply
6 Tactical.PRIMSEQ
6 Library.separate
6 MATCH_COMPILER().bestColumn
6 Type.occurs
6 Fast_Lin_Arith().elim_var
6 Metis_Subsume.idCompare
6 Code_Symbol.thyname_of_const
6 Blast().fromRule
6 Proofterm.map_proof_same
6 Path.check_elem
6 Proofterm.fulfill_norm_proof
6 Name.invent
6 CODEGEN_PARSETREE().getVariablesInPatt
6 Term.declare_term_names
6 CODETREE_SIMPLIFIER().specialToGeneral
6 Markup.markup
6 Variable.new_fixed
6 MATCH_COMPILER().codeGenerateMatch
6 Variable.decl_type_occsT
7 Universal.tag
7 Symbol.is_ascii_digit
7 Real.toArbitrary
7 X86OUTPUTCODE().codeGenerate
7 Axclass.class_of_param
7 Thm.eq_assumption
7 Thm.add_instT
7 CODETREE_LAMBDA_LIFT().checkBody
7 CODEGEN_PARSETREE().codeGenerate
7 Logic.nth_prem
7 Pretty.break_dist
7 Term_Subst.zero_var_indexes_inst
7 CODETREE_CODEGEN_CONSTANT_FUNCTIONS().cgFuns
7 Term.replace_types
7 Variable.variant_fixes
7 CODETREE_LAMBDA_LIFT().processBody
7 HashTable.hashSub
7 Scan.lift
7 Seq.empty
7 LEX_().parseToken
7 Type.cert_class
7 Raw_Simplifier.vperm
7 X86OUTPUTCODE().expandComplexOperations
7 IsaND.variant_names
7 Position.default
7 Scan.finite'
7 Thm.assumption
7 Library.string_of_int
7 Unify.clean_ffpair
7 Lazy.force_result
7 Type_Infer.paramify_vars
7 Real.scan
7 Future.join_results
8 Logic.list_all
8 Unify.head_of_in
8 CODETREE_OPTIMISER().lambdaLiftAndConstantFunction
8 Library.foldr
8 CODETREE_SIMPLIFIER().simpIfThenElse
8 Net.net_skip
8 Variable.decl_type_occs
8 Future.value_result
8 Metis_TermNet.mat
8 Tactical.CSUBGOAL
8 Variable.export_inst
8 Metis_ElementSet().foldl
8 Graph().restrict
8 Fast_Lin_Arith().split_items
8 Rat.common
8 Defs.restriction
8 Symbol_Pos.range
8 Single_Assignment.assign
8 Table().insert
8 Input.source_explode
8 CODETREE_OPTIMISER().evaluateInlining
8 Code_Thingol.annotate
8 Code_Thingol.translate_const
9 Real.fixFmt
9 Printer.pretty
9 Envir.expand_term
9 Pattern.proj
9 Table().insert_list
9 Type.strip_sorts
9 MATCH_COMPILER().pattCode
9 Metis_ElementSet().add
9 Library.enclose
9 Code_Thingol.translate_term
9 Proof_Context.replace_sortsT
9 Symbol_Pos.pad
9 CODETREE_OPTIMISER().optimise
9 Token.explode
9 Context.init_data
9 ThreadLib.protect
9 Pattern.match_bind
9 Blast().subst_bound
9 Name_Space.declare
10 Position.properties_of
10 Thm.implies_intr
10 Graph().get_entry
10 Generated_Code.netModel_node_propsd
10 X86OPTIMISE().generateCode
10 YXML.parse_chunk
10 X86OUTPUTCODE().opIndexedGen
10 Order_Tac.gen_order_tac
10 Term_Sharing.init
10 Unify.add_ffpair
10 Code.check_eqn
10 Metis_Subst.matchList
10 Thm.global_cterm_of
10 Proofterm.rewrite_prf
10 Code_Thingol.translate_const_proper
10 Synchronized.timed_access
11 Blast().aconv
11 Code_ML.print_sml_stmt
11 Lin_Arith.LA_Data.is_split_thm
11 stringEquality
11 Context.eq_thy_consistent
11 Sorts.subalgebra
11 Library.oo
11 Simplifier_Trace.mk_generic_result
11 Metis_KeyMap().treePeek
11 Thm.symmetric
11 Seq.flat
11 Term_Subst.map_types_same
11 Generated_Code.backlinks
11 Thm.fold_atomic_cterms
11 Metis_KeyMap().nodeUnion
11 Metis_Rule.repeatTopDownConv
11 Splitter().mk_case_split_tac
11 Lexicon.read_var
11 CODETREE_SIMPLIFIER().simpTuple
12 Context_Rules.del_rule0
12 Metis_Atom.compare
12 Metis_Subst.compose
12 Metis_Term.cmp
12 eq-xprod
12 Seq.maps
12 Blast().toTerm
12 Metis_KnuthBendixOrder.weightTerm
12 Term.could_beta_contract
12 Blast().tryClose
12 Fast_Lin_Arith().integ
12 Logic.strip_assums_hyp
12 UTILITIES_().splitString
12 Raw_Simplifier.var_perm
12 Seq.cons
12 ML_Compiler0.ml_input
12 Envir.above
13 CODETREE_STATIC_LINK_AND_CASES().staticLinkAndCases
13 Lin_Arith.LA_Data.decomp0
13 Pattern.ints_of
13 Thm.instantiate
14 Logic.count_prems
14 Unify.SIMPL0
14 Blast().norm
14 Value.parse_nat
14 Generated_Code.netModel_node_propsg
14 TYPE_TREE().generaliseTypes
14 Synchronized.value
14 List.partition
14 Metis_Subst.solve'
14 Generated_Code.subnets_host_attributes
14 Record.simproc
14 Graph().add_edge
14 Scan.:-
14 Sign.type_check
14 MATCH_COMPILER().intersect
14 Type_Constructor
15 Blast().add_term_vars
15 Unify.hounifiers
15 Code_Thingol.tag_term
15 Sorts.sort_le
15 Generated_Code.netModel_node_propsb
15 Term.type_of1
15 Unify.occurs_terms
16 HashArray.sub
16 Term.could_beta_eta_contract
16 Term_Position.decode
16 Pattern.mkabs
16 Code_Thingol.translate_typ
16 Type_Infer_Context.const_type
16 TYPECHECK_PARSETREE().pass2
17 Table().map_default
17 Code_Thingol.fold_constexprs
17 Scan.many
17 Pattern.flexrigid
17 Pattern.first_order
17 eq{...}
17 Name.desymbolize
17 Term.fold_atyps_sorts
17 Code_Thingol.ensure_tyco
17 Raw_Simplifier.uncond_skel
17 Thm.transitive
18 Thm.the_name_hint
18 Thm.strip_assums2
18 Unify.eta_norm
18 Proof_Context.arity_sorts
18 ML_Env.make_name_space
18 Table().update_new
18 Term_Ord.atoms_ord
18 Thm.make_context
19 Pattern.unify_types
19 Pattern.gen_rewrite_term
19 Pretty.make_block
19 Code.get_type_of_constr_or_abstr
19 Variable.map_data
19 Name.variant
19 Real.fromDecimal
19 Axclass.complete_classrels
19 String.implode
19 Library.eq_list
19 Table().update
19 Logic.incr_tvar_same
20 Proofterm.thm_ord
20 Symbol.is_ascii_blank
20 Sign.check_vars
20 Thm.lift_rule
20 CODETREE_SIMPLIFIER().simpFunctionCall
20 Logic.combound
21 Record.upd_simproc
21 Thm.norm_term_skip
21 Thm.could_bires
21 Library.?
21 Seq.append
21 Graph().reachable
21 Basics.cons
21 Blast().fromConst
22 Type.raw_match
22 Raw_Simplifier.rewrite_cterm
22 Thread_Data.setmp
22 Term.rename_abs
22 Thm.dest_state
23 Orders.struct_tac
23 Multithreading.sync_wait
23 Metis_Set.add
24 Name.declare
25 ML_Compiler0.ML
25 Table().del
25 Task_Queue.update_timing
25 Sorts.insert_term
25 Sorts.of_sort
26 Name_Space.merge
26 Thm.combination
26 Blast().unify
27 List.foldr
27 YXML.parse_body
27 Seq.it_right
28 X86ICodeGetConflictSets().getConflictStates
28 IntSet.partition
28 Proof_Data().map
28 CODETREE_SIMPLIFIER().simpNewenv
28 X86OUTPUTCODE().fixupLabels
28 Type.strip_constraints
28 Drule.is_norm_hhf
29 List.mapPartial
29 Sorts.coregular
29 eq-attr()
29 Print_Mode.print_mode_value
29 Code_Thingol.ensure_stmt
30 Generated_Code.new_configured_list_SecurityInvariant
30 X86ICodeIdentifyReferences().getInstructionState
30 Table().default
30 Element.instT_subst
31 TYPE_TREE().copyType
31 Raw_Simplifier.cond_tracing'
32 YXML.split_string
32 X86CodetreeToICode().codeFunctionToX86
32 Same.commit
33 Term.add_vars
33 Defs.reduction
34 Metis_KeyMap().treeAppend
34 Envir.fastype
35 SHA1.digest_string_external
36 Library.first_field
36 PARSE_DEC().parseDec
37 Symbol_Pos.explode
37 Type_Infer_Context.prepare_typ
37 Term_Ord.sort_ord
37 Thm.biresolution
38 Blast().prove
38 Table().map_table
38 Term_Subst.generalizeT_same
38 Logic.strip_imp_prems
38 CODETREE_SIMPLIFIER().simpLambda
39 Type.unified
40 Properties.put
40 X86ICodeToX86Code().icodeToX86Code
40 Timing.result
40 Logic.dest_equals
41 Table().fold_rev_table
41 Consts.certify
41 Axclass.unoverload_conv
41 Library.~~
42 CODETREE_SIMPLIFIER().simpGeneral
43 Term.could_unify
43 Generated_Code.map_filter
43 X86AllocateRegisters().allocateRegisters
43 Basics.#>>
43 Scan.>>
44 Thread.ConditionVar.innerWait
44 Symbol.is_ascii_letter
45 Parser.add_prods
45 IntSet.minusLists
46 TYPE_TREE().unifyTypes
46 AList.lookup
46 Binding.name_spec
46 Term.dest_abs
46 Metis_KeyMap().nodePeekPath
47 Type_Infer_Context.prepare_term
47 Pretty.formatted
48 Code.get_type
48 Thm.dest_binop
48 Blast().fromTerm
48 Proof_Context.prepare_sorts_env
48 X86PushRegisters().addRegisterPushes
48 Thm.gen_match
49 Term_Subst.generalize_same
49 X86ICodeTransform().spillRegisters
49 X86OUTPUTCODE().generateCode
50 Symbol.bump_string
50 Pattern.occurs
50 Library.I
51 CODETREE_SIMPLIFIER().simpSpecial
51 Timing.start
51 Raw_Simplifier.extract_rews
51 Term.add_loose_bnos
51 Term.add_tvarsT
51 Term.match_bvs
52 Ord_List.insert
53 Pattern.unif
53 Pattern.cases
53 Library.untag_list
53 Scan.||
53 BaseCodeTree.mapCodetree
55 Unify.rigid_occurs_term
55 Proof_Context.contract_abbrevs
56 Type.unify
57 UNKNOWN
58 Type.the_decl
58 Generated_Code.generate_valid_topology_some
60 Logic.lift_all
60 Thread_Attributes.uninterruptible
60 Library.unsuffix
60 TYPE_TREE().eventual
62 Pattern.match_rew
63 Library.K
63 Metis_Subst.insert
63 Net.add_key_of_terms
64 Term.abstract_over
65 Substring.fields
67 Generated_Code.equal_lista
67 String.substring
67 Metis_Subst.subst
68 Table().join
68 LargeInt.fmt
69 Type.lookup
70 Envir.head_norm
70 Table().get_first
72 Type_Infer_Context.infer
72 Thm.dest_equals_rhs
72 Term.map_atyps
73 Thread_Attributes.with_attributes
74 Symbol.explode
76 Context_Rules.Rules.merge
77 CODETREE_REMOVE_REDUNDANT().cleanProc
78 Term.map_types
80 Config.declare
81 Term.maxidx_term
85 Parser.PROCESSS
85 Sorts.insert_typ
86 Defs.normalize
89 Basics.fold_map
90 Term_Subst.map_atypsT_same
93 Term_Subst.inst_same
100 Term_Ord.typ_ord
100 Type.could_match
101 Thm.transfer_cterm
102 Basics.fold_rev
103 Substring.tokens
103 List.@
104 Envir.norm_type0
106 Type.cert_typ_mode
107 IntSet.mergeLists
109 Library.maps
111 Library.mergesort
111 Type_Infer.add_parms
113 Type_Infer.add_names
116 Thm.bicompose_aux
122 Term_Ord.struct_ord
126 Basics.try
129 String.concat
130 X86ICodeIdentifyReferences().identifyRegisters
134 Library.space_explode
141 Axclass.unoverload
146 Envir.norm_term1
149 Type_Infer.finish
151 Term.exists_type
154 String.fields
156 Sorts.insert
162 Envir.norm_term2
174 Net.matching
176 Multithreading.synchronized
188 Logic.incr_indexes_same
189 Pattern.first_order_match
190 Ord_List.union
191 Library.insert
195 Parser.prods_for
199 Sorts.mg_domain
199 Term.exists_subterm
205 Generated_Code.equal_nata
209 Term.subst_bound
210 Code_Symbol.symbol_ord
211 Logic.list_implies
220 GARBAGE COLLECTION (copy phase)
228 Term_Subst.instT_same
242 Defs.match_args
250 GARBAGE COLLECTION (update phase)
262 Context.join_certificate
285 Type_Infer_Context.unify
292 Raw_Simplifier.insert_rrule
293 o
304 Type.typ_match
310 Table().fold_table
311 Generic_Data().get
311 Raw_Simplifier.empty_ss
314 Pattern.match
317 Raw_Simplifier.rewrite_rule_extra_vars
320 Term.fold_term_types
330 Term.fold_aterms
351 Term.maxidx_typ
354 Raw_Simplifier.decomp_simp
364 Term.fastype_of1
378 Basics.#>
386 <anon>
420 Same.map
430 Raw_Simplifier.bottomc
432 Term.argument_type_of
463 List.filter
482 Thm.deriv_rule2
504 Raw_Simplifier.rewritec
516 GARBAGE COLLECTION (mark phase)
531 Term.fold_atyps
558 Term.could_eta_contract
572 Net.insert
650 Thm.transfer
771 Raw_Simplifier.eq_rrule
846 Term_Ord.fast_indexname_ord
1072 eq-term
1139 List.map
1281 Term.aconv
1313 Generated_Code.remdups
1483 Basics.fold
1552 Term.exists_subtype
3209 eq-typ
3388 Table().modify
3875 Table().defined
4121 Generated_Code.filter
6297 Table().lookup_key
7364 GARBAGE COLLECTION (minor collection)
8350 GARBAGE COLLECTION (total)
-------------- next part --------------
Network_Security_Policy_Verification:
1 HOLogic.mk_numeral
1 AList.map_index
1 Generated_Code.removeAll
1 Code_Preproc.add_classes
1 Global_Theory.name_multi
1 ForeignMemory.freeMem
1 Scan.provide
1 Scan.literal
1 Rule_Cases.lookup_cases_hyp_names
1 Thm.dest_all
1 Metis_Term.subtms
1 Code_Thingol.fold_varnames
1 Metis_Units.reduce
1 Metis_Waiting.cmp
1 Name_Space.check_reports
1 Syntax.parse_input
1 Locale.witness_add
1 Term.term_name
1 Proofterm.strip_shyps_proof
1 Pattern.clash
1 Library.chop_common_prefix
1 Metis_Useful.total
1 Metis_LiteralSet.subst
1 Lin_Arith.LA_Data.subst_term
1 TYPE_TREE().compareLabels
1 Thm.rule_attribute
1 ListPair.mapEq
1 Output_Primitives.ignore_outputs
1 Metis_KeyMap().compareIterator
1 CODETREE_CODEGEN_CONSTANT_FUNCTIONS().codeGenerate
1 antisym_le_simproc
1 Generated_Code.netModel_node_props
1 Generated_Code.plus_num
1 Toplevel.node_case
1 Table().exists
1 LEX_().initial
1 Constant
1 Syntax_Phases.mark_atoms
1 CODETREE_OPTIMISER().optLambda
1 BNF_LFP_Tactics.mk_alg_min_alg_tac
1 CODEGEN_PARSETREE().codeMatch
1 Proof.end_proof
1 Variable.polymorphic_types
1 Code_Thingol.translate_case
1 Blast().subst_atomic
1 Proof_Context.put_thms
1 Metis_Subsume.idSetAddMax
1 Metis_Active.simplify
1 Scan.first
1 HOLogic.dest_number
1 Syntax_Phases.markup_const
1 Pretty.getSimplePrinter
1 Blast().raw_blast
1 Code_Thingol.unfoldr
1 Auto_Bind.strip_judgment
1 Metis_Generate.metis_term_of_atp
1 Library.andf
1 Variable.markup_fixed
1 Code.expand_eta
1 Local_Defs.gen_unfold
1 CODETREE_SIMPLIFIER().simpArbitraryCompare
1 Value.parse_int
1 Metis_Proof.reconstructEquality
1 Code.handle_strictness
1 Generic_Target.notes
1 DEBUGGER_().makeValDebugEntries
1 BNF_LFP_Rec_Sugar.find_rec_calls
1 Classical().addbefore
1 CODETREE_OPTIMISER().useToPattern
1 Code_Preproc.trans_comb
1 Thm.of_class
1 Metis_Rewrite.rewriteIdLiteralsRule'
1 Lin_Arith.LA_Data.abstract_rel
1 Expression.declare_elem
1 Task_Queue.enqueue
1 Syntax.merge_syntax
1 UTILITIES_().checkForDots
1 Group_Cancel.add_atoms
1 Inductive.prove_elims
1 CODETREE_SIMPLIFIER().mkEnv
1 Library.order_list
1 Metis_Atom.subterm
1 Thm.cprem_of
1 Library.uncurry
1 Orders.order_tac
1 Blast().delete_concl
1 Metis_TermNet.filter
1 Thm.strip_apply
1 Scan.drain
1 PolyCompareArbitrary
1 Clasimp().nodup_depth_tac
1 Lin_Arith.LA_Data.filter_prems_tac_items
1 Conv.abs_conv
1 Local_Theory.background_theory_result
1 Numeral_Simprocs.dest_coeff
1 Variable.declare_constraints
1 STRUCTURES_().pass2Struct
1 Outer_Syntax.ship
1 Code.concretify_abs
1 Name.reject_internal
1 Record.record_fields_tr
1 Blast().log
1 LibraryIOSupport.wrapBinInFileDescr
1 Metis_Reconstruct.lookth
1 Graph().del_node
1 Parser.get_states
1 PolyThreadMutexBlock
1 Pretty.marks_str
1 Code.raw_assert_eqn
1 CODETREE_SIMPLIFIER().simpArbitraryArith
1 Metis_ElementSet().toList
1 Proof_Context.retrieve
1 Envir.binder_types
1 Code_Thingol.ensure_inst
1 Proof.current_goal
1 String_Code.add_literal_string
1 Fast_Lin_Arith().mkthm
1 Future.assign_result
1 X86OUTPUTCODE().codeCreate
1 Name_Space.hide
1 Pretty.newline
1 Sorts.inter_class
1 Local_Syntax.update_syntax
1 VALUE_OPS().displaySig
1 Fast_Lin_Arith().refutes
1 Metis_Rule.rem
1 Token.is_eof
1 SKIPS_().testfor
1 PolyRealBoxedFromString
1 Syntax.apply_tr'
1 Toplevel.apply_tr
1 polyCompiler
1 Syntax_Phases.free_or_skolem
1 Scan.recover
1 Syntax_Phases.decode_term
1 Latex.enclose_body
1 TextIO.TextStreamIO.output
1 Seq.maps_results
1 Metis_Thm.chk
1 Unify.sort_args
1 Library.replicate_string
1 Metis_Rule.mk_edges
1 Token.map_value
1 Term.no_dummy_patterns
1 Goal.PREFER_GOAL
1 Thy_Output.output_text
1 Syntax_Phases.parse_term
1 CODETREE_STATIC_LINK_AND_CASES().codeGenerate
1 LEX_().parseString
1 HOLogic.dest_bin
1 Pretty.mark
1 MATCH_COMPILER().pattDepth
1 Global_Theory.note_thmss
1 Parse.arguments
1 Variable.revert_bounds
1 Tactical.COND
1 Thm.abstract_rule
1 Goal.precise_conjunction_tac
1 Facts.add_static
1 Trancl_Tac().trancl_tac
1 Parser.produce
1 Code_Preproc.extend_arities_eqngr
1 Code_ML.ml_program_of_program
1 Metis_KeyMap().treeMap
1 Latex.output_symbols
1 Global_Theory.enter_thms
1 Attrib.attribute_cmd
1 Numeral.dest_num_syntax
1 Class.synchronize_inst_syntax
1 Proof_Context.check_const
1 Hypsubst().blast_hyp_subst_tac
1 Specification.get_positions
1 HOLogic.mk_number
1 CODETREE_OPTIMISER().codetreeOptimiser
1 Metis_Rule.everyLiterule
1 Token.explode
1 Lin_Arith.LA_Data.negated_term_occurs_positively
1 Code_Scala.print_scala_stmt
1 Overloading.improve_term_check
1 Net.dest
1 Splitter().split_thm_info
1 ATP_Proof_Reconstruct.robust_const_num_type_args
1 Code_Preproc.switch_trace
1 Variable.import_inst
1 Code_Thingol.ensure_class
1 Simpdata.mk_atomize
1 Fast_Lin_Arith().multiply_ineq
1 ML_Env.SML_environment
1 Record.dest_recTs
1 Misc_Legacy.add_term_names
1 MATCH_COMPILER().makeNaive
1 Proof.assert_bottom
1 PolyML.prettyPrint
1 VALUE_OPS().applyFunction
1 Char.isSpace
1 TYPEIDCODE().applyToInstance'
1 Generated_Code.sinvara
1 Fast_Lin_Arith().simpset_lin_arith_tac
1 Tactical.THEN'
1 Seq.map
1 PolyRealRound
1 SIGNATURES().sigVal
1 Value.parse_bool
1 Application
1 Library.take
1 Pattern.mapbnd
1 Numeral_Simprocs.numterms_ord
1 ATP_Util.stringN_of_int
1 Syntax_Phases.term_to_ast
1 Calculation.calculate
1 UniversalTable.univEnter
1 Nat_Numeral_Simprocs.find_first_coeff
1 Symbol.is_printable
1 Sign.gen_add_consts
1 Type.build_tsig
1 Metis_Rewrite.mkNeqConv
1 Induct().atomize_cterm
1 Future.join
1 Ord_List.remove
1 Element.inst_subst
1 Scan.extend_lexicon
1 Thm.undeclared_hyps
1 Value.print_real
1 Seq.first_result
1 Thm.map_tags
1 Scan.finite'
1 Specification.prep_decls
1 Assumption.add_assms
1 Element.eq_morphism
1 VALUE_OPS().getPolymorphism
1 Code_Thingol.construct_dictionaries
1 Code_Evaluation.subst_termify_app
1 Fast_Lin_Arith().print_ineqs
1 Library.unprefix
1 Syntax_Trans.fun_ast_tr'
1 it-proc-list_neq
1 Global_Theory.register_proofs
1 Consts.constrain
1 Position.norm_props
1 Metis_Rule.joinEdge
1 Unify.ins_arg
1 Hypsubst().vars_gen_hyp_subst_tac
1 X86ICodeTransform().codeICodeFunctionToX86
1 Syntax_Phases.check_terms
1 Generated_Code.sinvar
1 Outer_Syntax.parse_command
1 Simpdata.unsafe_solver_tac
1 Future.promise_name
1 Simplifier.simp
1 Metis_TermNet.termToQterm
1 Order_Tac.mkconcl_partial
1 Thm.forall_intr
1 STRUCT_VALS().makeLook
1 Token.scan_token
1 Seq.INTERVAL
1 CODETREE_CODEGEN_CONSTANT_FUNCTIONS().codeGenerateToConstant
1 Type.arity_sorts
1 Syntax_Phases.prune_types
1 Code_Target.prepare_serializer
1 EqSubst.clean_unify_z
1 Type_Infer.fixate
1 Pretty.separate
1 Misc_Legacy.add_typ_tvars
1 Mixfix.mixfix_args
1 Change_Table().merge
1 Order_Tac.mkasm_linear
1 Local_Defs.def_export
1 Envir.insert_sorts
1 Sorts.minimal_sorts
1 Metis_Subsume.insert
1 Classical().safe_step_tac
1 Local_Defs.contract
1 Method.METHOD
1 Future.forks
1 Code.check_decl_ty
1 Pattern.flexflex2
1 Token.transform
1 CODETREE().newLevel
1 Blast().add_loose_bnos
1 Metis_Rewrite.rewrIdConv'
1 Toplevel.app
1 TYPE_TREE().maptoRecord
1 Tactical.CHANGED
1 Syntax.update_syntax
1 ATP_Problem_Generate.add_iterm_syms_to_sym_table
1 Logic.has_meta_prems-ex_meta
1 Library.nth
1 Symbol_Pos.is_identifier
1 MATCH_COMPILER().buildAot
1 Toplevel.proofs'
1 ListPair.unzip
1 Real.fmt
1 Graph().irreducible_preds
1 Classical().addSafter
1 Tactic.biresolution_from_nets_tac
1 CODETREE_OPTIMISER().bodyReturnsTuple
1 CODEGEN_PARSETREE().codeSequence
1 Library.upto
1 UniversalTable.fold
1 Thm.equal_elim
1 Command.resolve_files
1 Proofterm.unconstrainT_body
1 Class.instantiation
1 Code_Thingol.exists_var
1 Toplevel.presentation_context
1 Metis_Reconstruct.inst_inference
1 Metis_KnuthBendixOrder.weightLowerBound
1 Proof_Context.gen_fixes
1 Raw_Simplifier.is_full_cong
1 Syntax.remove_syntax
1 Lexicon.tokenize
1 Induct().concl_var
1 Case_Translation.strip_case_full
2 Term.strip_abs_eta
2 X86OUTPUTCODE().largeWordToBytes
2 Token.reports
2 Local_Defs.fixed_abbrev
2 Theory.check_def
2 Toplevel.node_of
2 tabulate'
2 Code_Thingol.add_constsyms
2 Code.const_typ
2 Table().map_entry
2 Toplevel.atom_result
2 Meson.skolemize_with_choice_theorems
2 Variable.gen_all
2 Metis_Subsume.nonunitSubsumes
2 Private_Output.default_escape
2 Name_Space.extern
2 String.convString
2 Term_Ord.types_ord
2 Thm.rotate_rule
2 Parser.add_production
2 Sorts.add_arities_table
2 Blast().prune
2 DEBUGGER_().updateDebugLocation
2 Primitive_Defs.abs_def
2 Metis_TermNet.add
2 Meson.rename_bound_vars_RS
2 Variable.def_type
2 Tactical.no_tac
2 ATP_Problem_Generate.unascii_of-un
2 Envir.decr
2 Search.DEPTH_FIRST
2 Syntax.input_range
2 Code_Symbol.base_rel
2 Graph().diff_edges
2 Thm.dest_abs
2 Thy_Output.present_span
2 Goal.restrict
2 Thm.forall_elim
2 Raw_Simplifier.simp_trace_depth_limit_raw
2 Metis_Rule.transEqn
2 Task_Queue.status
2 Variable.add_fixes_binding
2 Scan.one
2 BaseCodeTree.foldtree
2 PRINT_TABLE().getOverloads
2 Library.chop
2 Printer.pretty_typ_ast
2 Blast().fromSubgoal
2 Name_Space.mandatory_prefixes1
2 eq-kind
2 PolyThreadMutexUnlock
2 Thm.plain_prop_of
2 CODEGEN_PARSETREE().reportUnreferencedValue
2 Name_Space.alias
2 Parse.keyword_markup
2 ATP_Problem_Generate.introduce_proxies_in_iterm
2 Change_Table().join
2 Fast_Lin_Arith().elim
2 Assumption.export
2 Parser.earley
2 Metis_Rule.fact
2 Options.check_name
2 Build.inline_message
2 Variable.declare_names
2 Private_Output.default_output
2 Code_Thingol.contains_dict_var
2 Method.CONTEXT_TACTIC
2 Balanced_Tree.dest
2 Code.desymbolize_tvars
2 Toplevel.apply_union
2 Trancl_Tac.decomp
2 Metis_Map.treeAppend
2 Metis_Subst.compatible
2 ML_Syntax.print_pair
2 Goal.future_result
2 Logic.dest_conjunctions
2 Lin_Arith.LA_Data.decomp_typecheck
2 Unify.get_eta_var
2 Term.map_type_tfree
2 Lin_Arith.LA_Data.allows_lin_arith
2 Thm.theory_of_thm
2 Unsynchronized.setmp
2 Item_Net.retrieve_matching
2 Term_Subst.zero_var_inst
2 Code_Printer.printer_of_mixfix
2 X86OUTPUTCODE().getConstant
2 Term.fold_subtypes
2 Simplifier.solve_all_tac
2 Proofterm.fulfill_proof_future
2 TYPE_TREE().copyTypeConstrWithCache
2 Proof_Context.check_type_name
2 Method.insert_tac
2 Seq.list_of
2 Token.inner_syntax_of
2 Unify.assignment
2 Basics.#->
2 Raw_Simplifier.simp_trace_raw
2 Tactical.REPEAT_DETERM_N
2 Blast().trace_prover
2 Thy_Output.present_thy
2 Outer_Syntax.command_reports
2 CODETREE().bottomLevel
2 Metis_ElementSet().firstl
2 Term.typ_subst_TVars
2 Fast_Lin_Arith().elim_var
2 Metis_Literal.subst
2 Syntax_Phases.parse_tree
2 Simplifier_Trace.check_breakpoint
2 Token.make_source
2 Thm.consolidate_theory
2 Named_Target.operations
2 Metis_Subsume.idCompare
2 Library.pair
2 Code_Namespace.prep_symbol
2 List_to_Set_Comprehension.simproc
2 Library.map2
2 Path.eval
2 Unify.flexargs
2 Proof_Context.standard_typ_check
2 Theory.dependencies
2 Code_Thingol.is_constr
2 Token.reports_of_value
2 PolyTimingGeneral
2 PRINT_TABLE().getOverload
2 Lin_Arith.LA_Data.add_atom
2 Code_Thingol.translate_app_const
2 Syntax_Phases.mark_aprop
2 TYPE_TREE().checkForEscapingDatatypes
2 Char.contains
2 Unify.matchers
2 Generated_Code.taintingTrusted_offending_list
2 Element.instantiate_tfrees
2 Misc.lookupDefault
2 Numeral.mk_num_syntax
2 Lin_Arith.LA_Data.pre_decomp
2 Variable.invent_types
2 Future.future_job
2 PARSE_TYPE().parseType
2 CODEGEN_PARSETREE().getVariablesInPatt
2 Proof_Context.prepare_sorts
2 Clasimp().mk_auto_tac
2 Code_Thingol.annotate_eqns
2 Timing.protocol_message
2 Term.declare_term_names
2 Pretty.enclose
2 Type_Constructor
2 Generic_Target.import_export_proof
2 Position.report_text
2 ML_Statistics.get
2 Code.get_head
2 Proof_Context.update_thms
3 Future.report_status
3 Seq.chop
3 Task_Queue.ready_job
3 Build.protocol_message
3 Blast().addLit
3 Syntax_Phases.unparse_t
3 Axclass.insert_arity_completions
3 X86OUTPUTCODE().opToInt
3 String.tokens
3 Logic.flatten_params
3 TYPE_TREE().makeEquivalent
3 UTILITIES_().searchList
3 Token.syntax_generic
3 Library.nth_map
3 Ord_List.subtract
3 Generated_Code.sinvarg
3 Blast().netMkRules
3 Metis_KeyMap().treeUnionDomain
3 Pretty.string
3 Class.synchronize_class_syntax
3 List.tabF
3 Metis_Map.treeIntersectDomain
3 SKIPS_().getid
3 Unify.change_bnos
3 Term.loose_bvar1
3 Code.eqn_conv
3 Envir.body_type
3 Name_Space.entry_markup
3 Thm.assume_hyps
3 Metis_ElementSet().foldl
3 Drule.comp_no_flatten
3 Metis_Rule.firstConv
3 Scan.dest
3 Arith_Data.simplify_meta_eq
3 Syntax_Phases.check
3 Code_Preproc.add_cert
3 Generated_Code.nonInterference_host_attributes
3 CODETREE_CODEGEN_CONSTANT_FUNCTIONS().cgLambda
3 Drule.zero_var_indexes_list
3 BasicStreamIO().input'
3 ProofRewriteRules.rew
3 Consts.the_constraint
3 Variable.variant_fixes
3 Proof.assert_mode
3 TYPE_TREE().tDisp
3 Proofterm.prepare_thm_proof
3 Symbol_Pos.source
3 Code_Preproc.get_node
3 Asn1.getNext
3 Metis_KeyMap().treePeek
3 Outer_Syntax.parse
3 Tactical.EVY
3 Seq.empty
3 Thm.varifyT_global'
3 Term_Ord.term_ord
3 Rat.make
3 Type.cert_class
3 Options.check_type
3 Metis_Rule.rewrConv
3 Element.map_ctxt
3 CODETREE_FUNCTIONS().findEntryInBlock
3 Future.join_next
3 Term.size_of_term
3 Fast_Lin_Arith().mklineq
3 IsaND.variant_names
3 Thy_Output.output_token
3 Symbol.beginning
3 Spec_Rules.Rules.empty
3 VALUE_OPS().codeVal
3 Real.genFmt
3 Term.binder_types
3 Blast().incr_bv
3 Case_Translation.check_case
3 CancelNumeralsFun().proc
3 Thm.dest_equals_lhs
3 Latex.output_name
3 Ast.match
3 Table().insert
3 Code_Thingol.unfoldl
3 Morphism.morphism
3 Library.split_last
3 Token.space_symbol
3 Proofterm.map_proof_same
3 Symbol.spaces
3 Metis_Subsume.genClauseSubsumes
3 exists_p_split
3 Axclass.overload_conv
3 Toplevel.transition
3 Goal.prove_common
3 Morphism.app
3 Code.equations_of_cert
3 Blast().fromIntrRule
3 Rule_Cases.extract_case
3 Proof_Context.map_data_result
3 VectorSliceOperations().subslice
3 Code_Runtime.value
3 X86OUTPUTCODE().rexByte
3 Numeral_Simprocs.numterm_ord
3 Unify.rigid_bound
3 Blast().subst_bound
3 UTILITIES_().noDuplicates
3 Symbol.bump_init
3 Blast().varOccur
3 Defs.merge
3 Markup.markup
3 Thm.incr_indexes
3 Thm.fold_atomic_ctyps
3 Proof_Context.expand_binds
4 Context.init_new_data
4 HashTable.hashSet
4 Symbol_Pos.stopper
4 Metis_Rule.everyConv
4 BinIO.openIn
4 it-proc
4 CODETREE_SIMPLIFIER().simpUnary
4 Thm.adjust_maxidx_thm
4 Symbol.decode
4 Metis_Atom.compare
4 Term.subst_bounds
4 Logic.remove_params
4 Lin_Arith.LA_Data.domain_is_nat
4 ML_Pretty.from_polyml-convert
4 Thm.implies_intr
4 Execution.fork
4 Name.bound
4 Generated_Code.integer_of_num
4 Logic.unvarifyT_global_same
4 Graph().get_entry
4 Pretty.blanks
4 Context.eq_thy_consistent
4 Syntax_Phases.parsetree_to_ast
4 EXPORT_PARSETREE().getExportTree
4 Lin_Arith.add_arith_facts
4 TYPE_TREE().allowGeneralisation
4 Trancl_Tac().rtrancl_tac
4 Ast.normalize
4 Printer.pretty
4 Envir.expand_term
4 Type.strip_sorts
4 Proofterm.make_thm_node
4 Variable.constrain_tvar
4 Fast_Lin_Arith().split_items
4 CODETREE_LAMBDA_LIFT().processBody
4 Simplifier_Trace.mk_generic_result
4 Library.enclose
4 Type_Infer_Context.prepare_positions
4 Proof_Context.def_type
4 YXML.push
4 Proof_Context.replace_sortsT
4 Code.check_eqn
4 Tactical.ALLGOALS
4 Simplifier_Trace.simp_apply
4 CODETREE_SIMPLIFIER().simpBinary
4 Library.separate
4 Position.default
4 Parser.movedot_lambda
4 Symbol.is_ascii_identifier
4 Thm.dest_comb
4 Address.stringOfWord
4 Tactical.ORELSE
4 MATCH_COMPILER().bestColumn
4 STRUCTURES_().gencodeStructs
4 Type_Infer.param_maxidx
4 Term_Subst.map_types_same
4 Lin_Arith.LA_Data.decomp_negation
4 Code_Symbol.prefix
4 Blast().fromRule
4 String.concatWith
4 Term.incr_bv
4 Envir.subst_type0
4 Metis_KeyMap().nodeUnion
4 Raw_Simplifier.congc
4 Fast_Lin_Arith().prove
4 Pattern.match_bind
4 Library.downto
4 Lazy.force_result
4 Conv.gconv_rule
4 Name_Space.intern'
4 Metis_Rule.pathConv
4 SKIPS_().skipon
4 Real.scan
4 ListPair.zip
4 Variable.new_fixed
5 Logic.list_all
5 Thm.rename_bvs
5 Future.worker_exec
5 Name_Space.make_accesses
5 CODETREE_SIMPLIFIER().simpIfThenElse
5 Table().delete_safe
5 Config.declare_option
5 Code_Thingol.translate_app
5 Context.invoke
5 Proofterm.add_npvars'
5 Drule.comp
5 X86OUTPUTCODE().opIndexedGen
5 it-setup
5 Blast().toTerm
5 Generated_Code.trancl_list_impl
5 Generated_Code.netModel_node_propsa
5 Sorts.subalgebra
5 Term.could_beta_contract
5 Token.is_symid
5 Simplifier_Trace.recurse
5 SymSet.++
5 Latex.output_sym
5 Tactical.PRIMSEQ
5 Defs.restriction
5 Future.broadcast
5 Type_Infer_Context.prepare
5 Type.occurs
5 Generated_Code.backlinks
5 Thm.permute_prems
5 Generated_Code.taint_labels
5 Path.check_elem
5 Proofterm.fulfill_norm_proof
5 Sorts.of_sort_derivation
5 Future.fulfill_result
5 Library.prefix
5 CODETREE_SIMPLIFIER().specialToGeneral
5 Variable.import
5 Task_Queue.dequeue_deps
6 Real.toArbitrary
6 Sorts.witness_sorts
6 Lin_Arith.LA_Data.is_split_thm
6 StronglyConnected.stronglyConnectedComponents
6 Generated_Code.netModel_node_propsd
6 Metis_TermNet.mat
6 Logic.nth_prem
6 Seq.maps
6 Code_Thingol.translate_typ
6 Value.parse_nat
6 CODETREE_SIMPLIFIER().simplifier
6 Code_Preproc.ensure_fun
6 LEX_().isAlphaNumeric
6 Metis_Tactic.kbo_advisory_simp_ordering
6 Tactical.ORELSE'
6 Thy_Header.read_header
6 Rat.common
6 Library.map_index
6 MATCH_COMPILER().plus
6 Thm.add_inst
6 Envir.eta
6 Hypsubst().eq_var
6 Splitter().cmap_of_split_thms
6 Symbol_Pos.range
6 Raw_Simplifier.check_conv
6 Metis_TermNet.qm
6 Logic.unconstrainT
6 Thm.global_cterm_of
6 Asn1.readHeader
6 List_to_Set_Comprehension.dest_case
6 Code_Printer.intro_base_names
6 Lin_Arith.LA_Data.decomp0
6 Term_Ord.atoms_ord
6 TYPECHECK_PARSETREE().setLeastGeneralTypes
6 Future.scheduler_loop
6 Axclass.get_info
6 TYPEIDCODE().TypeVarMap.mapTypeVars
6 CODETREE_FUNCTIONS().makeConstVal
6 Code_Thingol.translate_const
6 MATCH_COMPILER().codeGenerateMatch
7 Symbol.is_ascii_digit
7 Term.map_aterms
7 Code_Symbol.default_base
7 Type.varify_global
7 Thm.eq_assumption
7 Unify.SIMPL
7 LEX_().parseIdent
7 CODEGEN_PARSETREE().codeGenerate
7 Conv.fconv_rule
7 Variable.export_inst
7 CODETREE_CODEGEN_CONSTANT_FUNCTIONS().cgFuns
7 eq-loadForm
7 Code_Preproc.const_ord
7 Command.reports_of_token
7 Metis_Atom.match
7 Scan.lift
7 Unify.add_ffpair
7 Raw_Simplifier.vperm
7 CODETREE_FUNCTIONS().setInline
7 Context.init_data
7 Axclass.unoverload_const
7 Generated_Code.bLP_offending_list
7 CODEGEN_PARSETREE().codeFunBindings
7 Graph().add_edge
7 convStats
7 Tactical.THEN
7 Raw_Simplifier.var_perm
7 Seq.cons
7 Method.parser
7 Simplifier_Trace.step
7 Future.join_results
7 Variable.decl_type_occsT
8 eq-xsymb
8 Logic.lift_abs
8 CODETREE_LAMBDA_LIFT().checkBody
8 eq-xprod
8 Term.declare_typ_names
8 exists_paired_all
8 Pattern.proj
8 MATCH_COMPILER().pattCode
8 Code_Printer.gen_print_app
8 Thm.symmetric
8 Fast_Lin_Arith().integ
8 Proofterm.rewrite_prf
8 Thm.assumption
8 UTILITIES_().splitString
8 Code.add_rhss_of_eqn
8 Thm.make_context
8 Properties.seconds
8 Type_Infer.paramify_vars
8 ML_Compiler.report_parse_tree
8 Metis_Rule.repeatConv
9 CODETREE_OPTIMISER().lambdaLiftAndConstantFunction
9 List.concat
9 Thm.strip_shyps
9 Variable.decl_type_occs
9 Tactical.CSUBGOAL
9 Name.variant
9 Table().insert_list
9 Code_Thingol.translate_term
9 Simplifier.generic_simp_tac
9 Thm.could_bires
9 Code_Printer.make_vars
9 Logic.combound
9 Generated_Code.subnets_host_attributes
9 Record.simproc
9 Unify.clean_ffpair
9 Simpdata.mk_eq
9 Metis_Rule.repeatTopDownConv
9 Name_Space.declare
10 Raw_Simplifier.rewrite_cterm
10 YXML.parse_chunk
10 Pattern.first_order
10 Generated_Code.netModel_node_propsg
10 Logic.strip_params
10 Code_Namespace.hierarchical_program
10 X86OUTPUTCODE().expandComplexOperations
10 Scan.:-
10 MATCH_COMPILER().intersect
10 Library.string_of_int
10 Thm.generalize
10 Splitter().mk_case_split_tac
10 Envir.above
11 X86OPTIMISE().generateCode
11 Blast().norm
11 Blast().strip_imp_prems
11 Graph().restrict
11 Metis_KnuthBendixOrder.weightTerm
11 Term.replace_types
11 Code_Thingol.ensure_const
11 Metis_Subst.matchList
11 Thm.fold_atomic_cterms
11 Type_Infer_Context.const_type
11 CODETREE_OPTIMISER().evaluateInlining
12 Universal.tag
12 Context_Rules.del_rule0
12 Term_Position.decode
12 Net.net_skip
12 Future.value_result
12 Term_Subst.zero_var_indexes_inst
12 Pattern.flexrigid
12 Ctr_Sugar.morph_ctr_sugar
12 Order_Tac.gen_order_tac
12 TYPE_TREE().generaliseTypes
12 Axclass.complete_classrels
12 HashTable.hashSub
12 Term_Subst.map_aterms_same
12 Symbol_Pos.pad
12 Seq.flat
12 Single_Assignment.assign
12 Name.invent
12 CODETREE_SIMPLIFIER().simpTuple
13 Code_Thingol.fold_constexprs
13 Position.properties_of
13 Proof_Context.prepare_patternT
13 Thm.norm_term_skip
13 Term.fold_atyps_sorts
13 Blast().tryClose
14 Term.could_beta_eta_contract
14 Scan.many
14 Real.fixFmt
14 CODETREE_STATIC_LINK_AND_CASES().staticLinkAndCases
14 Library.oo
14 Term_Sharing.init
14 ML_Env.make_name_space
14 Pattern.ints_of
14 Raw_Simplifier.uncond_skel
15 X86OUTPUTCODE().codeGenerate
15 Orders.struct_tac
15 Proofterm.thm_ord
15 Logic.count_prems
15 Unify.hounifiers
15 Metis_ElementSet().add
15 ThreadLib.protect
15 Synchronized.timed_access
15 IntSet.addItem
15 Input.source_explode
16 ML_Compiler0.ML
16 Unify.clean_term
16 Pattern.mkabs
16 X86ICodeIdentifyReferences().getInstructionState
16 String.implode
16 Sign.type_check
16 Element.instT_subst
16 Metis_Set.add
16 Thm.transitive
16 Lexicon.read_var
17 Unify.head_of_in
17 stringEquality
17 Metis_Term.cmp
17 Sign.check_vars
17 CODETREE_SIMPLIFIER().simpFunctionCall
17 Synchronized.value
17 Library.?
17 CODETREE_OPTIMISER().optimise
17 Thm.instantiate
18 Blast().fromType
18 X86CodetreeToICode().codeFunctionToX86
18 Graph().reachable
18 Logic.strip_assums_hyp
19 HashArray.sub
19 Pattern.gen_rewrite_term
19 BasicStreamIO().flushOut'
19 Parser.prods_for
19 eq-attr()
19 eq{...}
20 Blast().aconv
20 Symbol.is_ascii_blank
20 Pretty.break_dist
20 Code_Thingol.ensure_stmt
20 Metis_Subst.solve'
20 Metis_Atom.unify
20 Table().default
20 Term.type_of1
20 Sorts.insert_term
20 ML_Compiler0.ml_input
21 LEX_().readChars
21 Thm.lift_rule
21 Name.desymbolize
21 Proof_Context.arity_sorts
22 Blast().add_term_vars
22 Code.get_type_of_constr_or_abstr
22 HashTable.hashValue
22 Thm.the_name_hint
22 Sorts.sort_le
22 Thm.strip_assums2
22 Logic.dest_equals
23 Term.rename_abs
23 Generated_Code.netModel_node_propsb
23 Type.strip_constraints
24 Unify.SIMPL0
24 Record.upd_simproc
24 Code_Thingol.tag_term
24 Thm.dest_state
24 Thm.combination
25 Table().map_default
25 Code_ML.print_sml_stmt
25 Pattern.unify_types
25 LEX_().parseToken
25 Unify.eta_norm
25 Code_Thingol.translate_const_proper
25 Term_Ord.sort_ord
25 Term_Subst.generalizeT_same
26 Metis_KeyMap().treeAppend
26 List.partition
26 Library.eq_list
26 Raw_Simplifier.cond_tracing'
26 Logic.strip_imp_prems
27 Generated_Code.map_filter
27 Code_Thingol.ensure_tyco
27 Unify.occurs_terms
28 Library.foldr
28 Properties.put
28 Term.add_vars
28 Blast().prove
28 Future.scheduler_next
28 Thread_Data.setmp
28 Real.fromDecimal
28 X86OUTPUTCODE().fixupLabels
28 YXML.parse_body
29 Generated_Code.tainiting_host_attributes
29 Envir.fastype
29 Consts.certify
29 Basics.cons
29 Logic.incr_tvar_same
30 IntSet.partition
30 YXML.split_string
30 Table().update
31 Binding.name_spec
31 Sorts.of_sort
31 Seq.it_right
32 Same.commit
33 Code.get_type
33 Metis_Subst.compose
33 Ord_List.insert
33 Name_Space.merge
34 List.mapPartial
34 X86ICodeToX86Code().icodeToX86Code
34 Seq.append
34 Blast().unify
35 Name.declare
35 X86ICodeTransform().spillRegisters
35 Type.the_decl
35 Proof_Context.prepare_sorts_env
35 Generated_Code.generate_valid_topology_some
35 Task_Queue.update_timing
35 Scan.||
36 Multithreading.sync_wait
36 SHA1.digest_string_external
36 List.foldr
36 Table().map_table
37 Library.first_field
37 X86AllocateRegisters().allocateRegisters
37 IntSet.minusLists
38 Basics.#>>
39 Library.~~
39 TYPECHECK_PARSETREE().pass2
40 CODETREE_SIMPLIFIER().simpNewenv
40 Table().del
40 Blast().fromConst
42 Print_Mode.print_mode_value
43 X86ICodeGetConflictSets().getConflictStates
43 Pretty.make_block
43 Term_Subst.generalize_same
43 Axclass.unoverload_conv
44 Table().fold_rev_table
44 CODETREE_SIMPLIFIER().simpLambda
45 CODETREE_SIMPLIFIER().simpGeneral
46 Raw_Simplifier.extract_rews
46 TYPE_TREE().copyType
46 Table().update_new
47 Generated_Code.new_configured_list_SecurityInvariant
47 Term.abstract_over
47 Timing.result
49 Drule.is_norm_hhf
50 Sorts.coregular
50 Scan.>>
51 Config.declare
51 BaseCodeTree.mapCodetree
52 Type.raw_match
52 Type_Infer_Context.prepare_typ
53 Symbol.bump_string
53 Defs.reduction
53 Thm.gen_match
54 Type_Infer_Context.prepare_term
54 Term.dest_abs
55 Thm.dest_binop
55 Net.add_key_of_terms
56 Pattern.unif
57 Logic.lift_all
57 Pattern.cases
57 X86PushRegisters().addRegisterPushes
57 Library.I
57 Term.match_bvs
58 Parser.PROCESSS
58 Term.add_tvarsT
58 X86OUTPUTCODE().generateCode
58 Thm.biresolution
58 Sorts.insert_typ
59 Type.unified
60 Symbol_Pos.explode
61 Term.could_unify
61 Lexicon.tokens_match_ord
62 Type.unify
62 Library.untag_list
62 TYPE_TREE().eventual
64 Thm.dest_equals_rhs
64 Term.map_atyps
65 Library.K
66 Term.add_loose_bnos
66 Library.unsuffix
67 Table().get_first
68 CODETREE_SIMPLIFIER().simpSpecial
68 LargeInt.fmt
69 Timing.start
69 Pattern.occurs
69 Unify.rigid_occurs_term
69 Substring.fields
71 Type_Infer_Context.infer
71 String.substring
72 Proof_Context.contract_abbrevs
72 Context_Rules.Rules.merge
73 Metis_Subst.subst
74 TYPE_TREE().unifyTypes
74 Metis_KeyMap().nodePeekPath
75 Symbol.explode
77 Basics.fold_map
77 Pattern.match_rew
81 PARSE_DEC().parseDec
83 Table().join
83 Symbol.is_ascii_letter
83 Pretty.formatted
83 Code_Symbol.thyname_of_const
84 Generated_Code.equal_nata
84 Type_Infer.add_parms
86 Thread_Attributes.uninterruptible
87 Term.map_types
88 Defs.normalize
89 Term_Subst.inst_same
90 CODETREE_REMOVE_REDUNDANT().cleanProc
90 Thread_Attributes.with_attributes
96 Term_Subst.map_atypsT_same
97 Term.maxidx_term
98 List.@
100 Metis_Subst.insert
101 Library.maps
102 Term_Ord.typ_ord
104 Term_Ord.struct_ord
104 Basics.fold_rev
104 Basics.try
109 Term.exists_type
110 String.concat
111 IntSet.mergeLists
112 Thm.transfer_cterm
113 Generated_Code.equal_lista
114 Substring.tokens
119 Axclass.unoverload
121 Type_Infer.finish
121 Envir.head_norm
121 Blast().fromTerm
121 Type_Infer.add_names
125 Type.could_match
127 Envir.norm_type0
134 UNKNOWN
137 Envir.norm_term2
139 Thm.bicompose_aux
140 Envir.norm_term1
143 Library.space_explode
149 Thread.ConditionVar.innerWait
149 Net.matching
156 Library.insert
156 Library.mergesort
156 Type.cert_typ_mode
158 X86ICodeIdentifyReferences().identifyRegisters
162 Term.subst_bound
166 Sorts.insert
171 Term.exists_subterm
172 String.fields
179 Pattern.first_order_match
187 Logic.list_implies
189 Generic_Data().get
200 GARBAGE COLLECTION (copy phase)
206 Defs.match_args
214 Logic.incr_indexes_same
216 Ord_List.union
221 GARBAGE COLLECTION (update phase)
223 Sorts.mg_domain
234 Term_Subst.instT_same
240 Raw_Simplifier.decomp_simp
248 Raw_Simplifier.empty_ss
251 Code_Symbol.symbol_ord
252 Context.join_certificate
282 Multithreading.synchronized
285 Term.fold_term_types
292 Type_Infer_Context.unify
297 Table().fold_table
301 Raw_Simplifier.rewrite_rule_extra_vars
302 Term.fold_aterms
307 Raw_Simplifier.insert_rrule
308 Pattern.match
323 Term.maxidx_typ
336 o
355 Thm.deriv_rule2
355 Basics.#>
362 <anon>
388 Same.map
408 Type.typ_match
413 Term.argument_type_of
425 List.filter
430 Raw_Simplifier.bottomc
466 Raw_Simplifier.rewritec
468 Term.could_eta_contract
470 Term.fastype_of1
490 Net.insert
518 GARBAGE COLLECTION (mark phase)
628 Thm.transfer
652 Term.fold_atyps
812 Raw_Simplifier.eq_rrule
885 eq-term
1066 List.map
1114 Term.aconv
1170 Term_Ord.fast_indexname_ord
1299 Generated_Code.remdups
1397 Table().lookup_key
1404 Term.exists_subtype
1417 Basics.fold
2959 eq-typ
3429 Table().modify
3998 Table().defined
4648 Generated_Code.filter
6098 Table().lookup
7989 GARBAGE COLLECTION (minor collection)
8928 GARBAGE COLLECTION (total)
13544 Generated_Code.equal_chara
29343 Generated_Code.divmod_integer
45490 IntInf.divMod
69982 Generated_Code.numeral
More information about the isabelle-dev
mailing list