Lines Matching refs:axioms
356 val axioms = e (content "axioms") #> many ((p name)
430 in oneOf [dt_type,consts,axioms,cls,
637 (* name * fixes * in-locale axioms *
638 ex-locale axioms * parents *)
658 (* axioms * theorems * consts *)
668 (* name * axioms * theorems * consts * datatypes *
691 (* name * axioms * theorems * consts * datatypes *
827 val axioms' = List.map (fn (n,t) => (n,(HOLogic.dest_Trueprop o #2
835 val axioms = List.map (fn (s,t) => (s,Term.subst_Vars sub_vars t))
836 axioms'
837 in (name,parents,axioms,#params i) end) cls_names end
861 val axioms' = List.filter
865 val axioms = List.map (fn (s,t) => (s,(HOLogic.dest_Trueprop o #2
867 o Thm.prop_of) t)) axioms'
881 List.exists (fn t' => t = t') in_locale_axioms) axioms
883 not (List.exists (fn t' => t = t') in_locale_axioms)) axioms
1095 val axioms = List.map (fn (n,t) => XML.Elem
1109 imports@axioms@theorems@consts@datatypes