equal
deleted
inserted
replaced
502 declaration {* |
502 declaration {* |
503 let |
503 let |
504 fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}] |
504 fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}] |
505 fun generic_whatis phi = |
505 fun generic_whatis phi = |
506 let |
506 let |
507 val [lt, le] = map (Morphism.term phi) |
507 val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}] |
508 (ProofContext.read_term_pats dummyT @{context} ["op \<sqsubset>", "op \<sqsubseteq>"]) (* FIXME avoid read? *) |
|
509 fun h x t = |
508 fun h x t = |
510 case term_of t of |
509 case term_of t of |
511 Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq |
510 Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq |
512 else Ferrante_Rackoff_Data.Nox |
511 else Ferrante_Rackoff_Data.Nox |
513 | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq |
512 | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq |